# HG changeset patch
# User blanchet
# Date 1380305615 -7200
# Node ID 16d9ecdf519a06698dd5f480e3bcc08ea609aee4
# Parent  949cef2095e236f368daea670ea1af4819b0ba1f
one more unfolding necessary

diff -r 949cef2095e2 -r 16d9ecdf519a src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Fri Sep 27 19:30:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Fri Sep 27 20:13:35 2013 +0200
@@ -71,7 +71,8 @@
     exclsss =
   mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
   mk_primcorec_cases_tac ctxt k m exclsss THEN
-  unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
+  unfold_thms_tac ctxt (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @
+    map_idents) THEN
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
     eresolve_tac falseEs ORELSE'
     resolve_tac split_connectI ORELSE'
@@ -112,5 +113,4 @@
      etac notE THEN' atac ORELSE'
      (TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac));
 
-
 end;