src/HOL/MiniML/Generalize.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4681 a331c1f5a23e
     1.1 --- a/src/HOL/MiniML/Generalize.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/MiniML/Generalize.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
     1.6    "gen ($ S A) ($ S t) <= $ S (gen A t)";
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (rename_tac "R" 1);
    1.10  by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
    1.11  by (typ.induct_tac "t" 1);
    1.12 @@ -105,7 +105,7 @@
    1.13  
    1.14  goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
    1.15    "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (rename_tac "S" 1);
    1.19  by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
    1.20  by (typ.induct_tac "t" 1);