diff -r 92d7d8e4f1bf -r 291934bac95e src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -158,14 +158,14 @@
           in
             (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
           end
-        val x = (Thm.cterm_of thy o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
+        val x = (Thm.global_cterm_of thy o the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
           Logic.dest_implies o Thm.prop_of) @{thm exI}
         fun prove_introrule (index, (ps, introrule)) =
           let
             val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
               THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
               THEN (EVERY (map (fn y =>
-                rtac (Drule.cterm_instantiate [(x, Thm.cterm_of thy (Free y))] @{thm exI}) 1) ps))
+                rtac (Drule.cterm_instantiate [(x, Thm.global_cterm_of thy (Free y))] @{thm exI}) 1) ps))
               THEN REPEAT_DETERM (rtac @{thm conjI} 1 THEN assume_tac ctxt' 1)
               THEN TRY (assume_tac ctxt' 1)
           in