--- a/src/HOLCF/FOCUS/Fstream.thy Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOLCF/FOCUS/Fstream.thy Mon Sep 06 19:13:10 2010 +0200
@@ -156,12 +156,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 [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
-apply (tactic {* step_tac (HOL_cs addSEs [thm "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 (HOL_cs addSEs @{thms DefE}) 1 *})
apply (erule contrapos_np)
apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
done