--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 18 16:09:02 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 18 16:09:15 2013 +0200
@@ -2011,11 +2011,17 @@
|> Thm.close_derivation
end;
+ val map_id0s_o_id =
+ map (fn thm =>
+ mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]}) @{thm id_o})
+ map_id0s;
+
val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
`split_conj_thm (split_conj_prems n
(mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
- |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o id_apply o_assoc sum_case_o_inj(1)} @
- map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
+ |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
+ map_id0s_o_id @ sym_map_comps)
+ OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
val timer = time (timer "corec definitions & thms");