--- a/src/HOL/Tools/datatype_prop.ML Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Sat Dec 01 18:52:32 2001 +0100
@@ -177,7 +177,7 @@
val used = foldr add_typ_tfree_names (recTs, []);
val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
- replicate (length descr') HOLogic.termS);
+ replicate (length descr') HOLogic.typeS);
val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -241,7 +241,7 @@
val recTs = get_rec_types descr' sorts;
val used = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
- val T' = TFree (variant used "'t", HOLogic.termS);
+ val T' = TFree (variant used "'t", HOLogic.typeS);
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -326,7 +326,7 @@
val recTs = get_rec_types descr' sorts;
val used' = foldr add_typ_tfree_names (recTs, []);
val newTs = take (length (hd descr), recTs);
- val T' = TFree (variant used' "'t", HOLogic.termS);
+ val T' = TFree (variant used' "'t", HOLogic.typeS);
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =