src/HOL/Library/Code_Abstract_Nat.thy

--- a/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:56:43 2015 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Fri Mar 06 23:57:01 2015 +0100
@@ -56,10 +56,9 @@
 
 fun remove_suc ctxt thms =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val vname = singleton (Name.variant_list (map fst
       (fold (Term.add_var_names o Thm.full_prop_of) thms []))) "n";
-    val cv = Thm.global_cterm_of thy (Var ((vname, 0), HOLogic.natT));
+    val cv = Thm.cterm_of ctxt (Var ((vname, 0), HOLogic.natT));
     val lhs_of = snd o Thm.dest_comb o fst o Thm.dest_comb o Thm.cprop_of;
     val rhs_of = snd o Thm.dest_comb o Thm.cprop_of;
     fun find_vars ct = (case Thm.term_of ct of