diff -r 5c25a2012975 -r 0eade173f77e src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/Pure/codegen.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -277,7 +277,7 @@
 
 fun preprocess_term thy t =
   let
-    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
+    val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
     (* fake definition *)
     val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
       (Logic.mk_equals (x, t));
@@ -459,7 +459,7 @@
 
 fun rename_terms ts =
   let
-    val names = List.foldr add_term_names
+    val names = List.foldr OldTerm.add_term_names
       (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
     val reserved = filter ML_Syntax.is_reserved names;
     val (illegal, alt_names) = split_list (map_filter (fn s =>
@@ -484,7 +484,7 @@
 (**** retrieve definition of constant ****)
 
 fun is_instance T1 T2 =
-  Type.raw_instance (T1, if null (typ_tfrees T2) then T2 else Logic.varifyT T2);
+  Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2);
 
 fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
   s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
@@ -598,7 +598,7 @@
 
 fun new_names t xs = Name.variant_list
   (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
-    add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
+    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
 
 fun new_name t x = hd (new_names t [x]);