[isabelle] Changing unification depth
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.
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
val search_bound = Config.int search_bound_value;
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and