method: syntax for SelectGoals;
authorwenzelm
Sat, 04 Mar 2006 21:10:11 +0100
changeset 19187 0c1ba28eaa17
parent 19186 1bf4b5c4a794
child 19188 a4c82a9ff7d8
method: syntax for SelectGoals;
src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sat Mar 04 21:10:10 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Sat Mar 04 21:10:11 2006 +0100
@@ -418,6 +418,7 @@
 and meth3 x =
  (meth4 --| $$$ "?" >> Method.Try ||
   meth4 --| $$$ "+" >> Method.Repeat1 ||
+  meth4 -- ($$$ "[" |-- nat --| $$$ "]") >> (Method.SelectGoals o swap) ||
   meth4) x
 and meth2 x =
  (position (xname -- args1 is_symid_meth false) >> (Method.Source o Args.src) ||