src/HOLCF/Lift.thy
changeset 32149 ef59550a55d3
parent 31076 99fe356cbbc2
child 35948 5e7909f0346b
--- a/src/HOLCF/Lift.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/Lift.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -61,7 +61,7 @@
 
 method_setup defined = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD'
-    (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
+    (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
 *} ""
 
 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"