# HG changeset patch
# User blanchet
# Date 1409777225 -7200
# Node ID f04e24a24fb9d0824760ab0629a07fe88d0ee408
# Parent  5777ec32682247596d0636ebad2cb708d26024e6
made new tactic even more robust

diff -r 5777ec326822 -r f04e24a24fb9 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
@@ -33,8 +33,8 @@
   DEEPEN (1, 64 (* large number *))
     (fn depth => meta_spec_mp_tac depth THEN' etac allE THEN' etac impE THEN' atac THEN' atac) 0;
 
-val same_ctr_simps =
-  @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split snd_conv simp_thms};
+val same_ctr_simps = @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split
+  id_apply snd_conv simp_thms};
 val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
 
 fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
@@ -42,7 +42,7 @@
       (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
     TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW
     REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW
-    use_induction_hypothesis_tac);
+    (atac ORELSE' use_induction_hypothesis_tac));
 
 fun distinct_ctrs_tac ctxt recs =
   HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));