# HG changeset patch
# User paulson
# Date 1100165200 -3600
# Node ID baa90469961a34de08d0d5e9e6f1b89524f5998c
# Parent  c18f5b076e5315f975e8f3edc8bcb4a8dec4d0ee
increased tracing and search bounds

diff -r c18f5b076e53 -r baa90469961a src/Pure/unify.ML
--- a/src/Pure/unify.ML	Mon Nov 08 16:53:50 2004 +0100
+++ b/src/Pure/unify.ML	Thu Nov 11 10:26:40 2004 +0100
@@ -35,8 +35,8 @@
 
 (*Unification options*)
 
-val trace_bound = ref 10	(*tracing starts above this depth, 0 for full*)
-and search_bound = ref 20	(*unification quits above this depth*)
+val trace_bound = ref 25	(*tracing starts above this depth, 0 for full*)
+and search_bound = ref 30	(*unification quits above this depth*)
 and trace_simp = ref false	(*print dpairs before calling SIMPL*)
 and trace_types = ref false	(*announce potential incompleteness
 				  of type unification*)