--- a/src/HOL/UNITY/Extend.ML Mon Aug 06 15:54:29 2001 +0200
+++ b/src/HOL/UNITY/Extend.ML Mon Aug 06 16:43:40 2001 +0200
@@ -753,14 +753,11 @@
by (auto_tac (claset(), simpset() addsimps [ok_def]));
qed "ok_extend_iff";
-Unify.search_bound := 40;
-Unify.trace_bound := 40;
-
-Goal "OK I (%i. extend h (F i)) = (OK I F)";
-by (auto_tac (claset(), simpset() addsimps [OK_def]));
+Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
+by Safe_tac;
by (dres_inst_tac [("x","i")] bspec 1);
-by (dres_inst_tac [("x","j")] bspec 2);
-by Auto_tac;
+by (dres_inst_tac [("x","j")] bspec 2);
+by (REPEAT (Force_tac 1));
qed "OK_extend_iff";
Goal "F : X guarantees Y ==> \