--- 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]);