src/HOL/BNF/Tools/bnf_lfp.ML
changeset 53138 4ef7d52cc5a0
parent 53106 d81211f61a1b
child 53143 ba80154a1118
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 22 11:30:14 2013 +0200
@@ -1862,6 +1862,7 @@
       ctor_injects = ctor_inject_thms, xtor_map_thms = folded_ctor_map_thms,
       xtor_set_thmss = folded_ctor_set_thmss', xtor_rel_thms = ctor_Irel_thms,
       xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
+      xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms],
       rel_co_induct_thm = Irel_induct_thm},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;