# HG changeset patch
# User oheimb
# Date 830433976 -7200
# Node ID b7078a395934ce1c2e3db79c5bba68f01031bd0b
# Parent  c67d543bc39569d2b0d3e06fc28f93ad42d8755e
temporarily included settings for unification bounds again

diff -r c67d543bc395 -r b7078a395934 src/HOL/MiniML/I.ML
--- a/src/HOL/MiniML/I.ML	Thu Apr 25 13:03:57 1996 +0200
+++ b/src/HOL/MiniML/I.ML	Thu Apr 25 14:06:16 1996 +0200
@@ -1,5 +1,8 @@
 open I;
 
+Unify.trace_bound := 45;
+Unify.search_bound := 50;
+
 goal thy
   "! a m s s' t n.  \
 \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \