# HG changeset patch
# User oheimb
# Date 830273129 -7200
# Node ID 8aff580dce443766d298c9ce48754f0c05006f30
# Parent  99044cda4ef349adeb61cd9ad9d421964365296c
*** empty log message ***

diff -r 99044cda4ef3 -r 8aff580dce44 src/HOL/MiniML/I.ML
--- a/src/HOL/MiniML/I.ML	Tue Apr 23 17:11:44 1996 +0200
+++ b/src/HOL/MiniML/I.ML	Tue Apr 23 17:25:29 1996 +0200
@@ -1,8 +1,5 @@
 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) -->   \