--- a/src/HOL/MiniML/Instance.ML Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/MiniML/Instance.ML Wed Nov 05 13:23:46 1997 +0100
@@ -50,7 +50,7 @@
\ (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
by (type_scheme.induct_tac "sch" 1);
by (Simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (rtac exI 1);
by (rtac ballI 1);
by (rtac sym 1);
@@ -62,10 +62,10 @@
by (dtac sym 1);
by (dtac sym 1);
by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
-by (safe_tac (claset()));
+by Safe_tac;
by (rename_tac "S1 S2" 1);
by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
by (strip_tac 1);
@@ -123,7 +123,7 @@
by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
by (asm_simp_tac (simpset() addsimps [aux2]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
by (type_scheme.induct_tac "sch" 1);
by (Simp_tac 1);
@@ -162,7 +162,7 @@
"(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
by (Simp_tac 1);
by (rtac iffI 1);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
by (eres_inst_tac [("x","0")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","Suc i")] allE 1);
@@ -220,7 +220,7 @@
by (type_scheme.induct_tac "sch" 1);
by (Simp_tac 1);
by (Simp_tac 1);
- by (SELECT_GOAL(safe_tac(claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
by (Asm_full_simp_tac 1);
by (Fast_tac 1);