1.1 --- a/src/Pure/Isar/method.ML	Tue Apr 29 15:25:50 2008 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Apr 29 19:55:02 2008 +0200
     1.3 @@ -79,6 +79,7 @@
     1.4    val method_setup: bstring -> string * Position.T -> string -> theory -> theory
     1.5    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
     1.6      -> src -> Proof.context -> 'a * Proof.context
     1.7 +  val simple_text: Args.T list -> text * Args.T list
     1.8    val simple_args: (Args.T list -> 'a * Args.T list)
     1.9      -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
    1.10    val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
    1.11 @@ -467,6 +468,11 @@
    1.12  
    1.13  fun syntax scan = Args.context_syntax "method" scan;
    1.14  
    1.15 +val simple_text = (Args.$$$ "(" |-- Args.name
    1.16 +    -- Scan.repeat (Scan.one (fn x => not (Args.string_of x = ")"))) --| Args.$$$ ")"
    1.17 +  || Args.name -- Scan.succeed [])
    1.18 +  >> (fn (name, args) => Source (Args.src ((name, args), Position.none)));
    1.19 +
    1.20  fun simple_args scan f src ctxt : method =
    1.21    fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
    1.22