src/HOL/Modelcheck/mucke_oracle.ML

--- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,3 @@
-
-(* $Id$ *)
 
 val trace_mc = ref false; 
 
@@ -250,7 +248,7 @@
    and thm.instantiate *)
 fun freeze_thaw t =
   let val used = add_term_names (t, [])
-          and vars = term_vars t;
+          and vars = OldTerm.term_vars t;
       fun newName (Var(ix,_), (pairs,used)) = 
           let val v = Name.variant used (string_of_indexname ix)
           in  ((ix,v)::pairs, v::used)  end;