src/ZF/ex/Primes.ML

--- a/src/ZF/ex/Primes.ML	Wed Nov 05 11:49:34 1997 +0100
+++ b/src/ZF/ex/Primes.ML	Wed Nov 05 13:14:15 1997 +0100
@@ -150,7 +150,7 @@
 by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right,
                                      dvd_imp_nat2]) 2);
 (* case x > 0 *)
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt,
                                      dvd_imp_nat2]) 1);
 by (eres_inst_tac [("x","a mod x")] ballE 1);