# HG changeset patch
# User traytel
# Date 1348765095 -7200
# Node ID 1a0f25c38629c61d69e587ea85aaf971f376671e
# Parent  a93f976c33078766f492ef37190d27abf3a5471c
tuned tactic; got rid of substs_tac alias

diff -r a93f976c3307 -r 1a0f25c38629 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Sep 27 18:58:15 2012 +0200
@@ -923,8 +923,7 @@
             (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
             val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
           in
-            Skip_Proof.prove lthy [] [] goal
-              (fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
+            Skip_Proof.prove lthy [] [] goal (K (mk_collect_set_natural_tac (#set_natural axioms)))
             |> Thm.close_derivation
           end;
 
diff -r a93f976c3307 -r 1a0f25c38629 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Sep 27 18:58:15 2012 +0200
@@ -8,7 +8,7 @@
 
 signature BNF_DEF_TACTICS =
 sig
-  val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
+  val mk_collect_set_natural_tac: thm list -> tactic
   val mk_id': thm -> thm
   val mk_comp': thm -> thm
   val mk_in_mono_tac: int -> tactic
@@ -44,8 +44,12 @@
     ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
   (etac subset_trans THEN' atac) 1;
 
-fun mk_collect_set_natural_tac ctxt set_naturals =
-  substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
+fun mk_collect_set_natural_tac set_naturals =
+  (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
+  EVERY' (map (fn set_natural =>
+    rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
+    rtac set_natural) set_naturals) THEN'
+  rtac @{thm image_empty}) 1;
 
 fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
   if null set_naturals then
diff -r a93f976c3307 -r 1a0f25c38629 src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 27 18:39:17 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Sep 27 18:58:15 2012 +0200
@@ -14,7 +14,6 @@
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val fo_rtac: thm -> Proof.context -> int -> tactic
   val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
-  val substs_tac: Proof.context -> thm list -> int -> tactic
   val unfold_thms_tac: Proof.context -> thm list -> tactic
   val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
 
@@ -62,7 +61,6 @@
 
 (*unlike "unfold_thms_tac", these succeed when the RHS contains schematic variables not in the LHS*)
 fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
-fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt NONE;
 
 
 (* Theorems for open typedefs with UNIV as representing set *)