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"