atomize_tac etc. moved to object_logic.ML;

--- a/src/Pure/Isar/method.ML	Sun Oct 14 20:09:19 2001 +0200
+++ b/src/Pure/Isar/method.ML	Sun Oct 14 20:09:59 2001 +0200
@@ -41,9 +41,6 @@
   val insert_facts: Proof.method
   val unfold: thm list -> Proof.method
   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
@@ -284,23 +281,6 @@
 fun fold thms = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac thms));
 
 
-(* atomize meta-connectives *)
-
-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 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;
-
-
 (* multi_resolve *)
 
 local