# 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'