Term.declare_term_frees;

--- a/src/Pure/Proof/proofchecker.ML	Wed Dec 31 19:54:03 2008 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Wed Dec 31 19:54:04 2008 +0100
@@ -30,8 +30,7 @@
 
 fun thm_of_proof thy prf =
   let
-    val prf_names = Proofterm.fold_proof_terms
-      (fold_aterms (fn Free (x, _) => Name.declare x | _ => I)) (K I) prf Name.context;
+    val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
     val lookup = lookup_thm thy;
 
     fun thm_of_atom thm Ts =

--- a/src/Tools/code/code_thingol.ML	Wed Dec 31 19:54:03 2008 +0100
+++ b/src/Tools/code/code_thingol.ML	Wed Dec 31 19:54:04 2008 +0100
@@ -707,8 +707,7 @@
         let
           val k = length ts;
           val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
-          val ctxt = (fold o fold_aterms)
-            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
+          val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context;
           val vs = Name.names ctxt "a" tys;
         in
           fold_map (translate_typ thy algbr funcgr) tys