diff -r 23f5cd23c1e1 -r 4cf8e86a2d29 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Wed Aug 02 18:33:46 2006 +0200
+++ b/src/Pure/codegen.ML	Wed Aug 02 22:26:37 2006 +0200
@@ -534,7 +534,7 @@
 fun rename_terms ts =
   let
     val names = foldr add_term_names
-      (map (fst o fst) (Drule.vars_of_terms ts)) ts;
+      (map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
     val reserved = names inter ThmDatabase.ml_reserved;
     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)