1.1 --- a/src/Pure/Isar/args.ML	Fri Mar 13 21:25:15 2009 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Fri Mar 13 23:32:40 2009 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4    val const: string context_parser
     1.5    val const_proper: string context_parser
     1.6    val bang_facts: thm list context_parser
     1.7 -  val goal_spec: ((int -> tactic) -> tactic) -> ((int -> tactic) -> tactic) context_parser
     1.8 +  val goal_spec: ((int -> tactic) -> tactic) context_parser
     1.9    val parse: token list parser
    1.10    val parse1: (string -> bool) -> token list parser
    1.11    val attribs: (string -> string) -> src list parser
    1.12 @@ -233,7 +233,7 @@
    1.13    $$$ "!" >> K ALLGOALS;
    1.14  
    1.15  val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
    1.16 -fun goal_spec def = Scan.lift (Scan.optional goal def);
    1.17 +fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
    1.18  
    1.19  
    1.20  (* arguments within outer syntax *)