--- 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.
--- 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)));
--- 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
--- 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));
--- 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;
--- 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")];
--- 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
--- 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);
--- 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))));
--- 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 *)
--- 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;
--- 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);
--- 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;
--- 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"),
--- 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 *)
--- 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))