1.1 --- a/src/Pure/Isar/args.ML	Tue Nov 10 14:38:06 2009 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Nov 10 14:38:39 2009 +0100
     1.3 @@ -223,7 +223,7 @@
     1.4  
     1.5  val bang_facts = Scan.peek (fn context =>
     1.6    P.position ($$$ "!") >> (fn (_, pos) =>
     1.7 -    (warning ("use of prems in proof method" ^ Position.str_of pos);
     1.8 +    (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos);
     1.9        Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
    1.10  
    1.11  val from_to =