diff -r a2d056424d3c -r 929984c529d3 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -105,11 +105,11 @@
         (map (fn ((((i, _), T), U), tname) =>
           make_pred i U T (mk_proj i is r) (Free (tname, T)))
             (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
-    val inst = map (apply2 (Thm.global_cterm_of thy)) (map head_of (HOLogic.dest_conj
+    val inst = map (apply2 (Thm.cterm_of ctxt)) (map head_of (HOLogic.dest_conj
       (HOLogic.dest_Trueprop (Thm.concl_of induct))) ~~ ps);
 
     val thm =
-      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems) (Thm.global_cterm_of thy concl)
+      Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems) (Thm.cterm_of ctxt concl)
         (fn prems =>
            EVERY [
             rewrite_goals_tac ctxt (map mk_meta_eq [@{thm fst_conv}, @{thm snd_conv}]),
@@ -185,12 +185,12 @@
     val y' = Free ("y", T);
 
     val thm =
-      Goal.prove_internal ctxt (map (Thm.global_cterm_of thy) prems)
-        (Thm.global_cterm_of thy
+      Goal.prove_internal ctxt (map (Thm.cterm_of ctxt) prems)
+        (Thm.cterm_of ctxt
           (HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))
         (fn prems =>
            EVERY [
-            rtac (cterm_instantiate [apply2 (Thm.global_cterm_of thy) (y, y')] exhaust) 1,
+            rtac (cterm_instantiate [apply2 (Thm.cterm_of ctxt) (y, y')] exhaust) 1,
             ALLGOALS (EVERY'
               [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
                resolve_tac ctxt prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])