1.1 --- a/src/Pure/Isar/args.ML	Mon Dec 18 08:21:34 2006 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Dec 18 08:21:35 2006 +0100
     1.3 @@ -84,9 +84,9 @@
     1.4      -> ((int -> tactic) -> tactic) * ('a * T list)
     1.5    val attribs: (string -> string) -> T list -> src list * T list
     1.6    val opt_attribs: (string -> string) -> T list -> src list * T list
     1.7 -  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
     1.8 +  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
     1.9    val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
    1.10 -    src -> Proof.context -> Proof.context * 'a
    1.11 +    src -> Proof.context -> 'a * Proof.context
    1.12  end;
    1.13  
    1.14  structure Args: ARGS =
    1.15 @@ -393,11 +393,11 @@
    1.16  
    1.17  fun syntax kind scan (src as Src ((s, args), pos)) st =
    1.18    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
    1.19 -    (SOME x, (st', [])) => (st', x)
    1.20 +    (SOME x, (st', [])) => (x, st')
    1.21    | (_, (_, args')) =>
    1.22        error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
    1.23          space_implode " " (map string_of args')));
    1.24  
    1.25 -fun context_syntax kind scan src = apfst Context.the_proof o syntax kind scan src o Context.Proof;
    1.26 +fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
    1.27  
    1.28  end;