# HG changeset patch
# User wenzelm
# Date 953657034 -3600
# Node ID 851d39c10d9fb9cb9cdc059091a8627dc8bf3eaa
# Parent  7c5fe9d1771230adca350238359b708622763396
goal_spec: [!];

diff -r 7c5fe9d17712 -r 851d39c10d9f src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Mar 21 17:32:44 2000 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 21 17:43:54 2000 +0100
@@ -151,7 +151,8 @@
 val from_to =
   nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
   nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
-  nat >> (fn i => fn tac => tac i);
+  nat >> (fn i => fn tac => tac i) ||
+  $$$$ "!" >> K ALLGOALS;
 
 val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
 fun goal_spec def = Scan.lift (Scan.optional goal def);