# HG changeset patch # User wenzelm # Date 1141503011 -3600 # Node ID 0c1ba28eaa17281be0c01e2b27cc516d9c9210c1 # Parent 1bf4b5c4a794db968fa1f45e28a1b2c2710b3e1c method: syntax for SelectGoals; diff -r 1bf4b5c4a794 -r 0c1ba28eaa17 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) ||