--- a/src/HOL/HOLCF/ex/Focus_ex.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/HOLCF/ex/Focus_ex.thy Thu Apr 18 17:07:01 2013 +0200
@@ -180,7 +180,8 @@
done
lemma lemma3: "def_g(g) --> is_g(g)"
-apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
+apply (tactic {* simp_tac (put_simpset HOL_ss @{context}
+ addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
apply (rule impI)
apply (erule exE)
apply (rule_tac x = "f" in exI)
@@ -204,7 +205,8 @@
done
lemma lemma4: "is_g(g) --> def_g(g)"
-apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
+apply (tactic {* simp_tac (put_simpset HOL_ss @{context}
+ delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
apply (rule impI)
apply (erule exE)