src/Pure/Isar/method.ML
changeset 23590 ad95084a5c63
parent 23577 c5b93c69afd3
child 23655 d2d1138e0ddc
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jul 05 19:59:01 2007 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jul 05 20:01:26 2007 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4  
     1.5  (* atomize rule statements *)
     1.6  
     1.7 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
     1.8 +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
     1.9    | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
    1.10  
    1.11  
    1.12 @@ -525,7 +525,7 @@
    1.13    bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option Args.nat))
    1.14      (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    1.15        HEADGOAL (insert_tac (prems @ facts) THEN'
    1.16 -      ObjectLogic.atomize_tac THEN' iprover_tac ctxt n)));
    1.17 +      ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
    1.18  
    1.19  end;
    1.20