src/HOL/HOLCF/ex/Focus_ex.thy
changeset 51717 9e7d1c139569
parent 41413 64cd30d6b0b8
child 55381 ca31f042414f
--- 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)