src/HOL/MiniML/Type.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4502 337c073de95e
--- a/src/HOL/MiniML/Type.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/MiniML/Type.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -444,7 +444,7 @@
 (* all greater variables are also new *)
 goalw thy [new_tv_def] 
   "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
-by (safe_tac (claset()));
+by Safe_tac;
 by (dtac spec 1);
 by (mp_tac 1);
 by (trans_tac 1);
@@ -547,7 +547,7 @@
 
 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
 by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (trans_tac 1);
 qed "less_maxL";