--- a/src/HOL/Tools/datatype_realizer.ML Mon Oct 25 17:19:17 2004 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Oct 26 16:25:41 2004 +0200
@@ -166,8 +166,6 @@
fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
let
val sg = sign_of thy;
- val sorts = map (rpair HOLogic.typeS) (distinct (flat (map
- (fn (_, (_, ds, _)) => mapfilter (try dest_DtTFree) ds) descr)));
val cert = cterm_of sg;
val rT = TFree ("'P", HOLogic.typeS);
val rT' = TVar (("'P", 0), HOLogic.typeS);