# HG changeset patch
# User wenzelm
# Date 951252685 -3600
# Node ID 58a33fd5b30c3710a057f038de087c73aa718580
# Parent  188e2924433e5a034780acde9bb4c29021a6e02d
tuned syntax wrapper;

diff -r 188e2924433e -r 58a33fd5b30c src/Pure/Isar/args.ML
--- 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))
diff -r 188e2924433e -r 58a33fd5b30c src/Pure/Isar/attrib.ML
--- 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);
diff -r 188e2924433e -r 58a33fd5b30c src/Pure/Isar/method.ML
--- 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);