1.1 --- a/src/Pure/Isar/args.ML	Tue Mar 21 17:32:44 2000 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Mar 21 17:43:54 2000 +0100
     1.3 @@ -151,7 +151,8 @@
     1.4  val from_to =
     1.5    nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
     1.6    nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
     1.7 -  nat >> (fn i => fn tac => tac i);
     1.8 +  nat >> (fn i => fn tac => tac i) ||
     1.9 +  $$$$ "!" >> K ALLGOALS;
    1.10  
    1.11  val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
    1.12  fun goal_spec def = Scan.lift (Scan.optional goal def);