# HG changeset patch
# User haftmann
# Date 1166426495 -3600
# Node ID a3efbae45735ef3a30515ec3c5c3de70692ab054
# Parent  cfc07819bb4713f6c4f16bc1fc784ef193db8d38
switched argument order in *.syntax lifters

diff -r cfc07819bb47 -r a3efbae45735 NEWS
--- a/NEWS	Mon Dec 18 08:21:34 2006 +0100
+++ b/NEWS	Mon Dec 18 08:21:35 2006 +0100
@@ -553,10 +553,10 @@
 property, add the corresponding classes.
 
 * Locale Lattic_Locales.partial_order changed (to achieve consistency with
-  axclass order):
-  - moved to Orderings.partial_order
-  - additional parameter ``less''
-  INCOMPATIBILITY.
+axclass order):
+- moved to Orderings.partial_order
+- additional parameter ``less''
+INCOMPATIBILITY.
 
 * Constant "List.list_all2" in List.thy now uses authentic syntax.
 INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar
@@ -768,6 +768,10 @@
 
 *** ML ***
 
+* Pure/Isar/args.ML & Pure/Isar/method.ML
+
+switched argument order in *.syntax lifters.
+
 * Pure/table:
 
 Function `...tab.foldl` removed.
diff -r cfc07819bb47 -r a3efbae45735 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -154,7 +154,7 @@
   Method.syntax
    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
     avoiding -- fixing -- rule_spec) src
-  #> (fn (ctxt, (((x, y), z), w)) =>
+  #> (fn ((((x, y), z), w), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
       HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
 
diff -r cfc07819bb47 -r a3efbae45735 src/HOL/Tools/function_package/auto_term.ML
--- a/src/HOL/Tools/function_package/auto_term.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -29,7 +29,7 @@
 
 
 val setup = Method.add_methods
-  [("relation", (Method.SIMPLE_METHOD' o uncurry relation_tac) oo (Method.syntax Args.term),
+  [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
     "proves termination using a user-specified wellfounded relation")]
 
 end
diff -r cfc07819bb47 -r a3efbae45735 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -440,7 +440,7 @@
 
 fun ind_cases src =
   Method.syntax (Scan.repeat1 Args.prop) src
-  #> (fn (ctxt, props) => Method.erule 0 (map (mk_cases ctxt) props));
+  #> (fn (props, ctxt) => Method.erule 0 (map (mk_cases ctxt) props));
 
 
 
diff -r cfc07819bb47 -r a3efbae45735 src/HOL/Tools/old_inductive_package.ML
--- a/src/HOL/Tools/old_inductive_package.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/Tools/old_inductive_package.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -583,7 +583,7 @@
 
 (* mk_cases_meth *)
 
-fun mk_cases_meth (ctxt, raw_props) =
+fun mk_cases_meth (raw_props, ctxt) =
   let
     val thy = ProofContext.theory_of ctxt;
     val ss = local_simpset_of ctxt;
diff -r cfc07819bb47 -r a3efbae45735 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/arith_data.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -1088,7 +1088,7 @@
     addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
     addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
   Method.add_methods
-    [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
+    [("arith", (arith_method o fst) oo Method.syntax Args.bang_facts,
       "decide linear arithmethic")] #>
   Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
     "declaration of split rules for arithmetic procedure")];
diff -r cfc07819bb47 -r a3efbae45735 src/HOL/ex/Reflection.thy
--- a/src/HOL/ex/Reflection.thy	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/HOL/ex/Reflection.thy	Mon Dec 18 08:21:35 2006 +0100
@@ -18,14 +18,14 @@
   fn src =>
     Method.syntax (Attrib.thms --
       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
-  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
+  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
 *} "partial automatic reification"
 
 method_setup reflection = {*
   fn src =>
     Method.syntax (Attrib.thms --
       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
-  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
+  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
 *} "reflection method"
 
 end
diff -r cfc07819bb47 -r a3efbae45735 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Provers/eqsubst.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -538,7 +538,7 @@
 the goal) as well as the theorems to use *)
 fun subst_meth src =
   Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
-  #> (fn (ctxt, ((asmflag, occL), inthms)) =>
+  #> (fn (((asmflag, occL), inthms), ctxt) =>
     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
 
 
diff -r cfc07819bb47 -r a3efbae45735 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Provers/induct_method.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -517,7 +517,7 @@
 fun cases_meth src =
   Method.syntax (Args.mode openN --
     (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
-  #> (fn (ctxt, (is_open, (insts, opt_rule))) =>
+  #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
     Method.METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
 
@@ -525,14 +525,14 @@
   Method.syntax (Args.mode openN --
     (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
     (arbitrary -- taking -- Scan.option induct_rule))) src
-  #> (fn (ctxt, (is_open, (insts, ((arbitrary, taking), opt_rule)))) =>
+  #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
 
 fun coinduct_meth src =
   Method.syntax (Args.mode openN --
     (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
-  #> (fn (ctxt, (is_open, ((insts, taking), opt_rule))) =>
+  #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
       Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
 
diff -r cfc07819bb47 -r a3efbae45735 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Provers/splitter.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -477,7 +477,7 @@
 
 fun split_meth src =
   Method.syntax Attrib.thms src
-  #> (fn (_, ths) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
+  #> (fn (ths, _) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
 
 
 (* theory setup *)
diff -r cfc07819bb47 -r a3efbae45735 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Pure/Isar/args.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -84,9 +84,9 @@
     -> ((int -> tactic) -> tactic) * ('a * T list)
   val attribs: (string -> string) -> T list -> src list * T list
   val opt_attribs: (string -> string) -> T list -> src list * T list
-  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
+  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
   val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
-    src -> Proof.context -> Proof.context * 'a
+    src -> Proof.context -> 'a * Proof.context
 end;
 
 structure Args: ARGS =
@@ -393,11 +393,11 @@
 
 fun syntax kind scan (src as Src ((s, args), pos)) st =
   (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
-    (SOME x, (st', [])) => (st', x)
+    (SOME x, (st', [])) => (x, st')
   | (_, (_, args')) =>
       error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
         space_implode " " (map string_of args')));
 
-fun context_syntax kind scan src = apfst Context.the_proof o syntax kind scan src o Context.Proof;
+fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
 
 end;
diff -r cfc07819bb47 -r a3efbae45735 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -185,7 +185,7 @@
 (** attribute syntax **)
 
 fun syntax scan src (st, th) =
-  let val (st', f) = Args.syntax "attribute" scan src st
+  let val (f, st') = Args.syntax "attribute" scan src st
   in f (st', th) end;
 
 fun no_args x = syntax (Scan.succeed x);
diff -r cfc07819bb47 -r a3efbae45735 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -115,7 +115,7 @@
 fun args scan f src node : string =
   let
     val loc = if ! locale = "" then NONE else SOME (! locale);
-    val (ctxt, x) = syntax scan src (Toplevel.presentation_context node loc);
+    val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
   in f src ctxt x end;
 
 
diff -r cfc07819bb47 -r a3efbae45735 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Pure/Isar/method.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -79,7 +79,7 @@
     -> theory -> theory
   val method_setup: bstring * string * string -> theory -> theory
   val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
-    -> src -> Proof.context -> Proof.context * 'a
+    -> src -> Proof.context -> 'a * Proof.context
   val simple_args: (Args.T list -> 'a * Args.T list)
     -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
@@ -459,10 +459,10 @@
 fun syntax scan = Args.context_syntax "method" scan;
 
 fun simple_args scan f src ctxt : method =
-  #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
+  fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
 
 fun ctxt_args (f: Proof.context -> method) src ctxt =
-  #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
+  fst (syntax (Scan.succeed (f ctxt)) src ctxt);
 
 fun no_args m = ctxt_args (K m);
 
@@ -486,7 +486,7 @@
 in
 
 fun sectioned_args args ss f src ctxt =
-  let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt
+  let val ((x, _), ctxt') = syntax (sectioned args ss) src ctxt
   in f x ctxt' end;
 
 fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
@@ -537,15 +537,15 @@
 (* tactic syntax *)
 
 fun nat_thms_args f = uncurry f oo
-  (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
+  (fst oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
 
-fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
+fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
 
 fun goal_args args tac = goal_args' (Scan.lift args) tac;
 
 fun goal_args_ctxt' args tac src ctxt =
-  #2 (syntax (Args.goal_spec HEADGOAL -- args >>
+  fst (syntax (Args.goal_spec HEADGOAL -- args >>
   (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
 
 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
@@ -562,7 +562,7 @@
   ("elim", thms_args elim, "repeatedly apply elimination rules"),
   ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
   ("fold", thms_ctxt_args fold_meth, "fold definitions"),
-  ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
+  ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
     "present local premises as object-level statements"),
   ("iprover", iprover_meth, "intuitionistic proof search"),
   ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
diff -r cfc07819bb47 -r a3efbae45735 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -349,7 +349,7 @@
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args f src ctxt =
-  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
+  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
 
 val insts_var =
   Scan.optional
@@ -357,7 +357,7 @@
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args_var f src ctxt =
-  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
+  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
 
 
 (* setup *)
diff -r cfc07819bb47 -r a3efbae45735 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Mon Dec 18 08:21:34 2006 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Mon Dec 18 08:21:35 2006 +0100
@@ -60,7 +60,7 @@
 
 (* ind_cases method *)
 
-fun mk_cases_meth (ctxt, props) =
+fun mk_cases_meth (props, ctxt) =
   props
   |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
     (ProofContext.read_prop ctxt))