changeset 44121 | 44adaa6db327 |
parent 43581 | c3e4d280bdeb |
child 45430 | b8eb7a791dac |
--- 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 ();