# HG changeset patch
# User wenzelm
# Date 1141839450 -3600
# Node ID ccdaf84bab5902e6fdce99ee4fe8dff45a893de6
# Parent  111ba44c66b2c01622ae21650e1085bcebc43c27
method: goal restriction defaults to [1];

diff -r 111ba44c66b2 -r ccdaf84bab59 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Mar 08 18:37:28 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Mar 08 18:37:30 2006 +0100
@@ -418,7 +418,7 @@
 and meth3 x =
  (meth4 --| $$$ "?" >> Method.Try ||
   meth4 --| $$$ "+" >> Method.Repeat1 ||
-  meth4 -- ($$$ "[" |-- nat --| $$$ "]") >> (Method.SelectGoals o swap) ||
+  meth4 -- ($$$ "[" |-- Scan.optional nat 1 --| $$$ "]") >> (Method.SelectGoals o swap) ||
   meth4) x
 and meth2 x =
  (position (xname -- args1 is_symid_meth false) >> (Method.Source o Args.src) ||