# HG changeset patch
# User traytel
# Date 1348830970 -7200
# Node ID 9b831f93d4e8e32e4ce25102c7ab2f55dcaa2810
# Parent  47431a27fefec943ab9450393c113982e3ab11d5
tuned tactic

diff -r 47431a27fefe -r 9b831f93d4e8 src/HOL/BNF/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Sep 28 11:46:57 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Sep 28 13:16:10 2012 +0200
@@ -77,7 +77,7 @@
     in
       (rtac udisc_exhaust THEN'
        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
-         EVERY' [if m = 0 then K all_tac else subst_tac ctxt NONE [uuncollapse] THEN' maybe_atac,
+         EVERY' [if m = 0 then K all_tac else rtac (uuncollapse RS trans) THEN' maybe_atac,
            rtac sym, rtac vdisc_exhaust,
            EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
              EVERY'
@@ -85,7 +85,7 @@
                   if m = 0 then
                     [hyp_subst_tac, rtac refl]
                   else
-                    [subst_tac ctxt NONE [vuncollapse], maybe_atac,
+                    [rtac (vuncollapse RS trans), maybe_atac,
                      if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
                      REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE, asm_simp_tac (ss_only [])]
                 else