# HG changeset patch
# User wenzelm
# Date 1003082999 -7200
# Node ID 4c45eb23ef68c1436ecb7713660513829c1a02ec
# Parent  fd780dd6e0b4b00032f281a0e2788a0c24f03a5c
atomize_tac etc. moved to object_logic.ML;

diff -r fd780dd6e0b4 -r 4c45eb23ef68 src/Pure/Isar/method.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