--- a/src/HOL/Hyperreal/NatStar.ML Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Hyperreal/NatStar.ML Thu Dec 13 15:45:03 2001 +0100
@@ -189,7 +189,7 @@
Goalw [congruent_def]
"congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})";
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS(Fuf_tac));
qed "starfunNat_congruent";
@@ -414,7 +414,7 @@
---------------------------------------------------------*)
Goalw [congruent_def]
"congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})";
-by (safe_tac (claset()));
+by Safe_tac;
by (ALLGOALS(Fuf_tac));
qed "starfunNat_n_congruent";