# HG changeset patch
# User wenzelm
# Date 965123727 -7200
# Node ID e56577a6300565c621480cd1ca832dd899c5c169
# Parent  3bda55143260f6631f5f3ec570f4183b80f8d21a
added atomize_goal / atomize_tac;

diff -r 3bda55143260 -r e56577a63005 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 01 00:20:12 2000 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 01 11:55:27 2000 +0200
@@ -39,6 +39,7 @@
   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 multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
   val resolveq_tac: thm Seq.seq -> int -> tactic
@@ -252,11 +253,15 @@
 
 (* atomize meta-connectives *)
 
-fun atomize_tac rews i st =
-  if Logic.has_meta_prems (#prop (Thm.rep_thm st)) i then
-    (warning "FIXME: atomize_tac";
-    Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews) i st)
-  else all_tac st;
+fun atomize_tac rews i thm =
+  if Logic.has_meta_prems (#prop (Thm.rep_thm thm)) i then
+    Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of rews) i thm
+  else all_tac thm;
+
+fun atomize_goal rews i thm =
+  (case Seq.pull (atomize_tac rews i thm) of
+    None => thm
+  | Some (thm', _) => thm');
 
 
 (* multi_resolve *)