Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made SML/NJ happier
authorblanchet
Wed, 07 Jan 2015 09:06:20 +0100
changeset 59314 91649ea1b32c
parent 59313 d7f4f46e9a59
child 59315 2f4d64fba0d7
child 59317 4ae9d8842597
made SML/NJ happier
src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Jan 07 00:10:23 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Jan 07 09:06:20 2015 +0100
@@ -69,7 +69,7 @@
    fun_defs: thm list,
    fpTs: typ list};
 
-fun morph_fp_rec_sugar phi {transfers, fun_names, funs, fun_defs, fpTs} =
+fun morph_fp_rec_sugar phi ({transfers, fun_names, funs, fun_defs, fpTs} : fp_rec_sugar) =
   {transfers = transfers,
    fun_names = fun_names,
    funs = map (Morphism.term phi) funs,
isabelle