Increasing the default limits in order to prevent unnecessary failures.
authorpaulson
Tue Sep 09 16:15:25 2008 +0200 (2008-09-09)
changeset 28173f7b5b963205e
parent 28172 a46751a649af
child 28174 626f0a79a4b9
Increasing the default limits in order to prevent unnecessary failures.
src/Pure/unify.ML
     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*)