# HG changeset patch
# User wenzelm
# Date 1011626116 -3600
# Node ID c92128238f85001106cc891a1b1d1aa21ef3c259
# Parent  57fb9d1ee34a69514aeee045df95ef7202d57e11
full_atomize;

diff -r 57fb9d1ee34a -r c92128238f85 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Jan 21 15:29:06 2002 +0100
+++ b/src/Pure/Isar/method.ML	Mon Jan 21 16:15:16 2002 +0100
@@ -182,6 +182,12 @@
 fun fold ths = SIMPLE_METHOD (CHANGED_PROP (fold_goals_tac ths));
 
 
+(* atomize rule statements *)
+
+fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)
+  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
+
+
 (* unfold intro/elim rules *)
 
 fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
@@ -640,7 +646,7 @@
   ("intro", thms_args intro, "repeatedly apply introduction rules"),
   ("elim", thms_args elim, "repeatedly apply elimination rules"),
   ("fold", thms_args fold, "fold definitions"),
-  ("atomize", no_args (SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)),
+  ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
     "present local premises as object-level statements"),
   ("rules", rules_args rules_meth, "apply many rules, including proof search"),
   ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
diff -r 57fb9d1ee34a -r c92128238f85 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Mon Jan 21 15:29:06 2002 +0100
+++ b/src/Pure/Isar/object_logic.ML	Mon Jan 21 16:15:16 2002 +0100
@@ -18,6 +18,7 @@
   val declare_rulify: theory attribute
   val atomize_term: Sign.sg -> term -> term
   val atomize_tac: int -> tactic
+  val full_atomize_tac: int -> tactic
   val atomize_goal: int -> thm -> thm
   val rulify: thm -> thm
   val rulify_no_asm: thm -> thm
@@ -135,6 +136,9 @@
     (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st
   else all_tac st;
 
+fun full_atomize_tac i st =
+  rewrite_goal_tac (get_atomize (Thm.sign_of_thm st)) i st;
+
 fun atomize_goal i st =
   (case Seq.pull (atomize_tac i st) of None => st | Some (st', _) => st');