diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -247,7 +247,7 @@
 (* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw
    and thm.instantiate *)
 fun freeze_thaw t =
-  let val used = add_term_names (t, [])
+  let val used = OldTerm.add_term_names (t, [])
           and vars = OldTerm.term_vars t;
       fun newName (Var(ix,_), (pairs,used)) = 
           let val v = Name.variant used (string_of_indexname ix)