src/Pure/codegen.ML

   let val {preprocs, ...} = CodegenData.get thy
   in fold (fn (_, f) => f thy) preprocs end;
 
 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));
     fun err () = error "preprocess_term: bad preprocessor"
   in case map prop_of (preprocess thy [eq]) of

 fun thyname_of_const thy =
   thyname_of thy (Consts.the_tags (Sign.consts_of thy));
 
 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 =>
       let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
     val ps = (reserved @ illegal) ~~

 
 
 (**** 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)));
 
 fun get_aux_code xs = map_filter (fn (m, code) =>

          separate (Pretty.brk 1) (p :: ps) @ [str ")"])
      else Pretty.block (separate (Pretty.brk 1) (p :: ps));
 
 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]);
 
 fun if_library x y = if member (op =) (!mode) "library" then x else y;