--- 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) --> \