diff -r 0a9fb49a086d -r 9d3ff36ad4e1 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Pure/Isar/args.ML	Sat Mar 06 15:39:16 2010 +0100
@@ -57,7 +57,6 @@
   val type_name: bool -> string context_parser
   val const: bool -> string context_parser
   val const_proper: bool -> string context_parser
-  val bang_facts: thm list context_parser
   val goal_spec: ((int -> tactic) -> tactic) context_parser
   val parse: token list parser
   val parse1: (string -> bool) -> token list parser
@@ -224,11 +223,6 @@
 
 (* improper method arguments *)
 
-val bang_facts = Scan.peek (fn context =>
-  P.position ($$$ "!") >> (fn (_, 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 =
   P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
   P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||