--- a/src/HOL/Tools/datatype_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -609,7 +609,7 @@
val size_names = DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
- val freeT = TFree (variant used "'t", HOLogic.typeS);
+ val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
let val Ts = map (typ_of_dtyp descr' sorts) cargs