diff -r aaba731fce86 -r ad95084a5c63 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jul 05 19:59:01 2007 +0200
+++ b/src/Pure/Isar/method.ML	Thu Jul 05 20:01:26 2007 +0200
@@ -196,7 +196,7 @@
 
 (* atomize rule statements *)
 
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
   | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
 
 
@@ -525,7 +525,7 @@
   bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
     (fn n => fn prems => fn ctxt => METHOD (fn facts =>
       HEADGOAL (insert_tac (prems @ facts) THEN'
-      ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)));
+      ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
 
 end;