# HG changeset patch
# User paulson
# Date 1220969725 -7200
# Node ID f7b5b963205e925e4def208d945b86a7b2758c46
# Parent  a46751a649afad9b46380c4f097f20019f8c3ec5
Increasing the default limits in order to prevent unnecessary failures.

diff -r a46751a649af -r f7b5b963205e src/Pure/unify.ML
--- a/src/Pure/unify.ML	Mon Sep 08 22:14:39 2008 +0200
+++ b/src/Pure/unify.ML	Tue Sep 09 16:15:25 2008 +0200
@@ -33,11 +33,11 @@
 (*Unification options*)
 
 (*tracing starts above this depth, 0 for full*)
-val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 25);
+val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 50);
 val trace_bound = Config.int trace_bound_value;
 
 (*unification quits above this depth*)
-val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 30);
+val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 60);
 val search_bound = Config.int search_bound_value;
 
 (*print dpairs before calling SIMPL*)