src/HOL/Tools/Datatype/datatype.ML
changeset 56254 a2dd9200854d
parent 56249 0fda98dd2c93
child 58111 82db9ad610b9
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -373,7 +373,7 @@
     1.4  
     1.5          fun mk_thm i =
     1.6            let
     1.7 -            val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
     1.8 +            val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t"));
     1.9              val f = Free ("f", Ts ---> U);
    1.10            in
    1.11              Goal.prove_sorry_global thy [] []