src/HOL/HOLCF/Tools/cont_proc.ML

--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Fri Mar 06 23:57:01 2015 +0100
@@ -121,8 +121,7 @@
 local
   fun solve_cont ctxt t =
     let
-      val thy = Proof_Context.theory_of ctxt
-      val tr = instantiate' [] [SOME (Thm.global_cterm_of thy t)] @{thm Eq_TrueI}
+      val tr = instantiate' [] [SOME (Thm.cterm_of ctxt t)] @{thm Eq_TrueI}
     in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end
 in
   fun cont_proc thy =