# HG changeset patch
# User wenzelm
# Date 979601352 -3600
# Node ID 51be80fc443987c600629525e888ec8fe7b084c7
# Parent  de95ba2760fe6bf2212abed15ced2b0c0e1a61f4
added atomize_strip_tac;

diff -r de95ba2760fe -r 51be80fc4439 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jan 16 00:28:50 2001 +0100
+++ b/src/Pure/Isar/method.ML	Tue Jan 16 00:29:12 2001 +0100
@@ -41,6 +41,7 @@
   val fold: thm list -> Proof.method
   val atomize_tac: thm list -> int -> tactic
   val atomize_goal: thm list -> int -> thm -> thm
+  val atomize_strip_tac: thm list * thm list -> int -> tactic
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
@@ -273,13 +274,16 @@
 
 (* atomize meta-connectives *)
 
-fun atomize_tac rews =
+fun atomize_strip_tac (rews, strip) =
   let val rew_tac = rewrite_goal_tac rews in
     fn i => fn thm =>
-      if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then rew_tac i thm
+      if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then
+        (rew_tac i THEN REPEAT (match_tac strip i)) thm
       else all_tac thm
   end;
 
+fun atomize_tac rews = atomize_strip_tac (rews, []);
+
 fun atomize_goal rews =
   let val tac = atomize_tac rews
   in fn i => fn thm => (case Seq.pull (tac i thm) of None => thm | Some (thm', _) => thm') end;