# HG changeset patch
# User traytel
# Date 1348999453 -7200
# Node ID 869c7a2e2945d0590c586d84d4f2e97871baa6f1
# Parent  f099b8006a3c083d5cea5badd48104f9626e7455
tuned tactic

diff -r f099b8006a3c -r 869c7a2e2945 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sat Sep 29 21:59:08 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Sun Sep 30 12:04:13 2012 +0200
@@ -141,9 +141,19 @@
       pre_set_defss mss (unflat mss (1 upto n)) kkss)
   end;
 
+local
+
+fun hhf_concl_conv cv ctxt ct =
+  (case Thm.term_of ct of
+    Const ("all", _) $ Abs _ => Conv.arg_conv (Conv.abs_conv (hhf_concl_conv cv o snd) ctxt) ct
+  | _ => Conv.concl_conv ~1 cv ct);
+
+in
+
 fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
   hyp_subst_tac THEN'
-  subst_tac ctxt (SOME [1, 2]) [ctr_def] THEN'
+  CONVERSION (hhf_concl_conv
+    (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN'
   (atac ORELSE' REPEAT o etac conjE THEN'
@@ -151,6 +161,8 @@
        (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms)) THEN_MAYBE'
      REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
 
+end;
+
 fun mk_coinduct_distinct_ctrs discs discs' =
   hyp_subst_tac THEN' REPEAT o etac conjE THEN'
   full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms));