diff -r 01de796250a0 -r 44adaa6db327 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Aug 10 20:12:36 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Aug 10 20:53:43 2011 +0200
@@ -398,7 +398,7 @@
         Syntax.string_of_typ ctxt T);
     fun type_of_constr (cT as (_, T)) =
       let
-        val frees = OldTerm.typ_tfrees T;
+        val frees = Misc_Legacy.typ_tfrees T;
         val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
           handle TYPE _ => no_constr cT
         val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();