src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML

 
     val cont_thm =
       let
         val prop = mk_trp (mk_cont functional)
         val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
-        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
-      in
-        Goal.prove_global thy [] [] prop (K tac)
+        fun tac ctxt = REPEAT_ALL_NEW (match_tac ctxt (rev rules)) 1
+      in
+        Goal.prove_global thy [] [] prop (tac o #context)
       end
 
     val tuple_unfold_thm =
       (@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
       |> Local_Defs.unfold (Proof_Context.init_global thy) @{thms split_conv}