# HG changeset patch
# User blanchet
# Date 1382283954 -7200
# Node ID 800106c1741954c5c5b53456fbd46fccdfaa47b9
# Parent  9b25747a134792f49d616b597adce60a5839eac4
avoid tactic failure for equations that contain an unapplied 'id'

diff -r 9b25747a1347 -r 800106c17419 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sat Oct 19 00:00:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 20 17:45:54 2013 +0200
@@ -81,7 +81,7 @@
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
-      (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @ map_idents)))));
+      (@{thms id_def o_def split_def sum.cases} @ maps @ map_comps @ map_idents)))));
 
 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
   HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'