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 10:06:51 +0100
changeset 55093 a4eafd0db804
parent 55092 f05b42b908f4
child 55094 149ccaf4ae5c
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 07:18:05 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Jan 21 10:06:51 2014 +0100
@@ -365,7 +365,7 @@
    (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss,
     disc_iter_iff_attrs),
    (map (map (map (Morphism.thm phi))) sel_unfoldsss,
-    map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
+    map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms;
 
 val transfer_gfp_sugar_thms =
   morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
isabelle