Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Datatype/datatype.ML
changeset 56254 a2dd9200854d
parent 56249 0fda98dd2c93
child 58111 82db9ad610b9 
--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 22 18:19:57 2014 +0100
@@ -373,7 +373,7 @@
 
         fun mk_thm i =
           let
-            val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
+            val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t"));
             val f = Free ("f", Ts ---> U);
           in
             Goal.prove_sorry_global thy [] []
isabelle