bang_facts: legacy feature;

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