--- a/src/Pure/Isar/args.ML Tue Feb 22 21:50:02 2000 +0100
+++ b/src/Pure/Isar/args.ML Tue Feb 22 21:51:25 2000 +0100
@@ -39,7 +39,7 @@
val dest_src: src -> (string * T list) * Position.T
val attribs: T list -> src list * T list
val opt_attribs: T list -> src list * T list
- val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
+ val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
end;
structure Args: ARGS =
@@ -183,7 +183,7 @@
(* argument syntax *)
-fun syntax kind scan st (src as Src ((s, args), pos)) =
+fun syntax kind scan (src as Src ((s, args), pos)) st =
(case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
OK (Some x, (st', [])) => (st', x)
| OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
--- a/src/Pure/Isar/attrib.ML Tue Feb 22 21:50:02 2000 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Feb 22 21:51:25 2000 +0100
@@ -157,7 +157,7 @@
(** attribute syntax **)
fun syntax scan src (st, th) =
- let val (st', f) = Args.syntax "attribute" scan st src
+ let val (st', f) = Args.syntax "attribute" scan src st
in f (st', th) end;
fun no_args x = syntax (Scan.succeed x);
--- a/src/Pure/Isar/method.ML Tue Feb 22 21:50:02 2000 +0100
+++ b/src/Pure/Isar/method.ML Tue Feb 22 21:51:25 2000 +0100
@@ -50,7 +50,7 @@
val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
-> theory -> theory
val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
- Proof.context -> Args.src -> Proof.context * 'a
+ Args.src -> Proof.context -> Proof.context * 'a
val ctxt_args: (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
type modifier
@@ -403,7 +403,7 @@
Args.syntax "method" scan;
fun ctxt_args (f: Proof.context -> Proof.method) src ctxt =
- #2 (syntax (Scan.succeed (f ctxt)) ctxt src);
+ #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
fun no_args m = ctxt_args (K m);
@@ -428,7 +428,7 @@
in
fun sectioned_args args ss f src ctxt =
- let val (ctxt', (x, _)) = syntax (sectioned args ss) ctxt src
+ let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt
in f x ctxt' end;
fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
@@ -447,7 +447,7 @@
Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --
(Scan.lift (Args.$$$ "in") |-- Attrib.local_thm);
-fun inst_args f src ctxt = f ((#2 oo syntax insts) ctxt src);
+fun inst_args f = f oo (#2 oo syntax insts);