src/HOL/Library/Code_Abstract_Nat.thy

--- a/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 10:10:38 2014 +0100
+++ b/src/HOL/Library/Code_Abstract_Nat.thy	Wed Feb 26 11:57:52 2014 +0100
@@ -50,8 +50,9 @@
 setup {*
 let
 
-fun remove_suc thy thms =
+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 = cterm_of thy (Var ((vname, 0), HOLogic.natT));