src/HOL/ex/Fib.ML
changeset 3724 f33e301a89f5
parent 3300 4f5ffefa7799
child 3919 c036caebfc75
--- a/src/HOL/ex/Fib.ML	Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/ex/Fib.ML	Mon Sep 29 11:37:02 1997 +0200
@@ -54,7 +54,7 @@
     (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, 
 				      mod_less, mod_Suc]
                             setloop split_tac[expand_if])));
-by (step_tac (!claset addSDs [mod2_neq_0]) 1);
+by (safe_tac (!claset addSDs [mod2_neq_0]));
 by (ALLGOALS
     (asm_full_simp_tac
      (!simpset addsimps (fib.rules @ add_ac @ mult_ac @