src/Pure/unify.ML
changeset 28173 f7b5b963205e
parent 26939 1035c89b4c02
child 29269 5c25a2012975
     1.1 --- a/src/Pure/unify.ML	Mon Sep 08 22:14:39 2008 +0200
     1.2 +++ b/src/Pure/unify.ML	Tue Sep 09 16:15:25 2008 +0200
     1.3 @@ -33,11 +33,11 @@
     1.4  (*Unification options*)
     1.5  
     1.6  (*tracing starts above this depth, 0 for full*)
     1.7 -val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 25);
     1.8 +val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 50);
     1.9  val trace_bound = Config.int trace_bound_value;
    1.10  
    1.11  (*unification quits above this depth*)
    1.12 -val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 30);
    1.13 +val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 60);
    1.14  val search_bound = Config.int search_bound_value;
    1.15  
    1.16  (*print dpairs before calling SIMPL*)