Fixed problem with sorts in function make_casedists.
authorberghofe
Tue Oct 26 16:25:41 2004 +0200 (2004-10-26)
changeset 152569237f388fbb1
parent 15255 1b860b5d23f8
child 15257 19dcdea98649
Fixed problem with sorts in function make_casedists.
src/HOL/Tools/datatype_realizer.ML
     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);