diff -r 92d7d8e4f1bf -r 291934bac95e src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Pure/Isar/code.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -363,7 +363,7 @@
 
 fun analyze_constructor thy (c, ty) =
   let
-    val _ = Thm.cterm_of thy (Const (c, ty));
+    val _ = Thm.global_cterm_of thy (Const (c, ty));
     val ty_decl = devarify (const_typ thy c);
     fun last_typ c_ty ty =
       let
@@ -611,7 +611,7 @@
     val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
       raw_vars;
     fun expand (v, ty) thm = Drule.fun_cong_rule thm
-      (Thm.cterm_of thy (Var ((v, 0), ty)));
+      (Thm.global_cterm_of thy (Var ((v, 0), ty)));
   in
     thm
     |> fold expand vars
@@ -681,7 +681,7 @@
 (* code equation certificates *)
 
 fun build_head thy (c, ty) =
-  Thm.cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty)));
+  Thm.global_cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty)));
 
 fun get_head thy cert_thm =
   let
@@ -716,7 +716,7 @@
     val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
     val ty = fastype_of lhs;
     val ty_abs = (fastype_of o snd o dest_comb) lhs;
-    val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs));
+    val abs = Thm.global_cterm_of thy (Const (c, ty --> ty_abs));
     val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm];
   in (c, (Thm.varifyT_global o zero_var_indexes) raw_concrete_thm) end;
 
@@ -804,7 +804,7 @@
       |> constrain_thm thy vs sorts;
     val head' = Thm.term_of head
       |> subst
-      |> Thm.cterm_of thy;
+      |> Thm.global_cterm_of thy;
     val cert_thm'' = cert_thm'
       |> Thm.elim_implies (Thm.assume head');
   in cert_thm'' end;