# HG changeset patch
# User traytel
# Date 1379022182 -7200
# Node ID 11a77e4aa98b8fff993c01c5c490bcdee3a1df9f
# Parent  3fb81ab13ea3be5993b2b767c8571496f82267c0
more robust tactic to cover another corner case (added as example);

diff -r 3fb81ab13ea3 -r 11a77e4aa98b src/HOL/BNF/Examples/Misc_Codatatype.thy
--- a/src/HOL/BNF/Examples/Misc_Codatatype.thy	Thu Sep 12 23:29:13 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy	Thu Sep 12 23:43:02 2013 +0200
@@ -73,6 +73,7 @@
 
 codatatype ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
 
+codatatype 'b poly_unit = U "'b \<Rightarrow> 'b poly_unit"
 codatatype 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
 
 codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs =
diff -r 3fb81ab13ea3 -r 11a77e4aa98b src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Sep 12 23:29:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Sep 12 23:43:02 2013 +0200
@@ -2014,7 +2014,7 @@
     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 o_assoc sum_case_o_inj(1)} @
+        |> 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]});
 
     val timer = time (timer "corec definitions & thms");
diff -r 3fb81ab13ea3 -r 11a77e4aa98b src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 12 23:29:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 12 23:43:02 2013 +0200
@@ -61,8 +61,7 @@
   |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
   |> mk_Trueprop_eq
   |> (fn goal => Goal.prove_sorry ctxt [] [] goal
-     (fn {context=ctxt, prems = _} =>
-       unfold_thms_tac ctxt [@{thm o_def}, mk_sym thm] THEN rtac refl 1))
+    (K (rtac ext 1 THEN unfold_thms_tac ctxt [o_apply, mk_sym thm] THEN rtac refl 1)))
   |> Thm.close_derivation;