src/HOL/Tools/Datatype/datatype_aux.ML

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Wed Aug 10 20:53:43 2011 +0200
@@ -144,7 +144,7 @@
     fun abstr (t1, t2) =
       (case t1 of
         NONE =>
-          (case flt (OldTerm.term_frees t2) of
+          (case flt (Misc_Legacy.term_frees t2) of
             [Free (s, T)] => SOME (absfree (s, T, t2))
           | _ => NONE)
       | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))