1.1 --- a/src/HOL/MiniML/Type.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/MiniML/Type.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -444,7 +444,7 @@
     1.4  (* all greater variables are also new *)
     1.5  goalw thy [new_tv_def] 
     1.6    "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (dtac spec 1);
    1.10  by (mp_tac 1);
    1.11  by (trans_tac 1);
    1.12 @@ -547,7 +547,7 @@
    1.13  
    1.14  goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
    1.15  by (simp_tac (simpset() addsplits [expand_if]) 1);
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (trans_tac 1);
    1.19  qed "less_maxL";
    1.20