# HG changeset patch
# User traytel
# Date 1379513355 -7200
# Node ID ee9eaab634e5a3ebe6c515988f987cbc00b29ff7
# Parent  a66d211ab34eb294670b514ca1b6fb64d65887a0
don't unfold as eager as in 11a77e4aa98b

diff -r a66d211ab34e -r ee9eaab634e5 src/HOL/BNF/Tools/bnf_gfp.ML
--- 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");