src/HOL/MiniML/Instance.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4641 70a50c2a920f
     1.1 --- a/src/HOL/MiniML/Instance.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/MiniML/Instance.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
     1.5  by (type_scheme.induct_tac "sch" 1);
     1.6  by (Simp_tac 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (rtac exI 1);
    1.10  by (rtac ballI 1);
    1.11  by (rtac sym 1);
    1.12 @@ -62,10 +62,10 @@
    1.13  by (dtac sym 1);
    1.14  by (dtac sym 1);
    1.15  by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (rename_tac "S1 S2" 1);
    1.19  by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
    1.20 -by (safe_tac (claset()));
    1.21 +by Safe_tac;
    1.22  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    1.23  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    1.24  by (strip_tac 1);
    1.25 @@ -123,7 +123,7 @@
    1.26  by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
    1.27  by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
    1.28  by (asm_simp_tac (simpset() addsimps [aux2]) 1);
    1.29 -by (safe_tac (claset()));
    1.30 +by Safe_tac;
    1.31  by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
    1.32  by (type_scheme.induct_tac "sch" 1);
    1.33  by (Simp_tac 1);
    1.34 @@ -162,7 +162,7 @@
    1.35    "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
    1.36  by (Simp_tac 1);
    1.37  by (rtac iffI 1);
    1.38 - by (SELECT_GOAL(safe_tac (claset()))1);
    1.39 + by (SELECT_GOAL Safe_tac 1);
    1.40    by (eres_inst_tac [("x","0")] allE 1);
    1.41    by (Asm_full_simp_tac 1);
    1.42   by (eres_inst_tac [("x","Suc i")] allE 1);
    1.43 @@ -220,7 +220,7 @@
    1.44  by (type_scheme.induct_tac "sch" 1);
    1.45    by (Simp_tac 1);
    1.46   by (Simp_tac 1);
    1.47 - by (SELECT_GOAL(safe_tac(claset()))1);
    1.48 + by (SELECT_GOAL Safe_tac 1);
    1.49   by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
    1.50   by (Asm_full_simp_tac 1);
    1.51   by (Fast_tac 1);