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/BNF/Tools/bnf_lfp_compat.ML
changeset 53808 b3e2022530e3
parent 53747 a8253329ebe9
child 53901 3d93e8b4ae02 
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Mon Sep 23 23:27:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Sep 24 00:01:10 2013 +0200
@@ -131,7 +131,7 @@
     val all_notes =
       (case lfp_sugar_thms of
         NONE => []
-      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) =>
+      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>
         let
           val common_notes =
             (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
isabelle