--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Fri May 13 22:55:00 2011 +0200
@@ -152,12 +152,12 @@
lemma slen_fscons_eq_rev:
"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
apply (simp add: fscons_def2 slen_scons_eq_rev)
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
+apply (tactic {* step_tac (put_claset HOL_cs @{context} addSEs @{thms DefE}) 1 *})
apply (erule contrapos_np)
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done