# HG changeset patch
# User berghofe
# Date 1098800741 -7200
# Node ID 9237f388fbb1c02a1b83f026aeddf97a84748821
# Parent  1b860b5d23f8059eef9a082a52013463c582429e
Fixed problem with sorts in function make_casedists.

diff -r 1b860b5d23f8 -r 9237f388fbb1 src/HOL/Tools/datatype_realizer.ML
--- 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);