src/HOL/HOLCF/Lift.thy
changeset 51717 9e7d1c139569
parent 49759 ecf1d5d87e5e
child 55417 01fbfb60c33e
     1.1 --- a/src/HOL/HOLCF/Lift.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/HOLCF/Lift.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5  method_setup defined = {*
     1.6    Scan.succeed (fn ctxt => SIMPLE_METHOD'
     1.7 -    (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
     1.8 +    (etac @{thm lift_definedE} THEN' asm_simp_tac ctxt))
     1.9  *}
    1.10  
    1.11  lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"