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/ZF/Tools/datatype_package.ML
changeset 44241 7943b69f0188
parent 44058 ae85c5d64913
child 46949 94aa7b81bcf6 
--- a/src/ZF/Tools/datatype_package.ML	Wed Aug 17 16:46:58 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Wed Aug 17 18:05:31 2011 +0200
@@ -235,7 +235,7 @@
       Misc_Legacy.mk_defpair
         (recursor_tm,
          @{const Univ.Vrecursor} $
-           absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
+           absfree ("rec", @{typ i}) (list_comb (case_const, recursor_cases)));
 
   (* Build the new theory *)
isabelle