--- 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 *)