src/HOL/Tools/datatype_realizer.ML
changeset 15256 9237f388fbb1
parent 14981 e73f8140af78
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Oct 25 17:19:17 2004 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Oct 26 16:25:41 2004 +0200
     1.3 @@ -166,8 +166,6 @@
     1.4  fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
     1.5    let
     1.6      val sg = sign_of thy;
     1.7 -    val sorts = map (rpair HOLogic.typeS) (distinct (flat (map
     1.8 -      (fn (_, (_, ds, _)) => mapfilter (try dest_DtTFree) ds) descr)));
     1.9      val cert = cterm_of sg;
    1.10      val rT = TFree ("'P", HOLogic.typeS);
    1.11      val rT' = TVar (("'P", 0), HOLogic.typeS);