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