[isabelle] Changing unification depth



Hi all,

I'm trying to increase the unification depth in the theory using
declare [[unification_search_bound = 70]], but it seems there's no
effect and stays at 60.

theory Test
imports Complex_Main
begin

declare [[unification_search_bound = 70]]
...

Using an unsynchronized reference, changing the last line of Unify.hounifiers to

in (ref := search_bnd; add_unify 1 ((env,dps), Seq.empty)) end;

and reading off ref, it still shows 60.

It seems that Unify.search_bound is fixed to the value of
Unify.search_bound_value, which is default to 60 due to

val search_bound_value = Config.declare true "unify_search_bound" (K
(Config.Int 60));
val search_bound = Config.int search_bound_value;
...
fun hounifiers...
   val search_bnd = Config.get_global thy search_bound
   ...
   if tdepth > search_bnd then
        (warning "Unification bound exceeded"; (Seq.pull reseq))
   ...

Any help will be appreciated.

Thanks

John





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.