src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
changeset 58957 c9e744ea8a38
parent 58936 7fbe4436952d
child 59498 50b60f501b05
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -151,9 +151,9 @@
     1.4        let
     1.5          val prop = mk_trp (mk_cont functional)
     1.6          val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
     1.7 -        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
     1.8 +        fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1
     1.9        in
    1.10 -        Goal.prove_global thy [] [] prop (K tac)
    1.11 +        Goal.prove_global thy [] [] prop (tac o #context)
    1.12        end
    1.13  
    1.14      val tuple_unfold_thm =