--- a/src/HOL/Induct/LFilter.ML Mon Sep 29 11:36:44 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML Mon Sep 29 11:37:02 1997 +0200
@@ -187,7 +187,7 @@
goal thy "lfilter p (lfilter p l) = lfilter p l";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
+by Safe_tac;
(*Cases: p x is true or false*)
by (Blast_tac 1);
by (rtac (lfilter_cases RS disjE) 1);
@@ -327,7 +327,7 @@
goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
+by Safe_tac;
by (Blast_tac 1);
by (case_tac "lmap f l : Domain (findRel p)" 1);
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);