# HG changeset patch
# User blanchet
# Date 1348235609 -7200
# Node ID a944eefb67e671c35629b93ec29e05cf97ee7343
# Parent  df9b897fb254fac17f0178f941ce24a1bbb3ba36
fixed bug introduced by fold/unfold renaming

diff -r df9b897fb254 -r a944eefb67e6 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -521,8 +521,8 @@
       in Term.list_comb (mapx, args) end;
 
     val mk_simp_thmss =
-      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn rec_likes =>
-        injects @ distincts @ cases @ rec_likes @ rec_likes);
+      map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
+        injects @ distincts @ cases @ rec_likes @ fold_likes);
 
     fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, ctr_defss,
         fold_defs, rec_defs), lthy) =