src/Pure/unify.ML
changeset 15275 baa90469961a
parent 14643 130076a81b84
child 15531 08c8dad8e399
     1.1 --- a/src/Pure/unify.ML	Mon Nov 08 16:53:50 2004 +0100
     1.2 +++ b/src/Pure/unify.ML	Thu Nov 11 10:26:40 2004 +0100
     1.3 @@ -35,8 +35,8 @@
     1.4  
     1.5  (*Unification options*)
     1.6  
     1.7 -val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
     1.8 -and search_bound = ref 20	(*unification quits above this depth*)
     1.9 +val trace_bound = ref 25	(*tracing starts above this depth, 0 for full*)
    1.10 +and search_bound = ref 30	(*unification quits above this depth*)
    1.11  and trace_simp = ref false	(*print dpairs before calling SIMPL*)
    1.12  and trace_types = ref false	(*announce potential incompleteness
    1.13  				  of type unification*)