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
Tue, 21 Jan 2014 13:13:02 +0100
changeset 55095 7883bd17362f
parent 55094 149ccaf4ae5c
child 55097 81dac5c1a5bb
made SML/NJ happier
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:05:22 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 13:13:02 2014 +0100
@@ -341,7 +341,8 @@
 
 fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
   ((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
-   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
+   (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs))
+  : lfp_sugar_thms;
 
 val transfer_lfp_sugar_thms =
   morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
isabelle