switched argument order in *.syntax lifters
authorhaftmann
Mon Dec 18 08:21:35 2006 +0100 (2006-12-18)
changeset 21879a3efbae45735
parent 21878 cfc07819bb47
child 21880 0ce06e95982a
switched argument order in *.syntax lifters
NEWS
src/HOL/Nominal/nominal_induct.ML
src/HOL/Tools/function_package/auto_term.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/old_inductive_package.ML
src/HOL/arith_data.ML
src/HOL/ex/Reflection.thy
src/Provers/eqsubst.ML
src/Provers/induct_method.ML
src/Provers/splitter.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/method.ML
src/Pure/Isar/rule_insts.ML
src/ZF/Tools/ind_cases.ML
     1.1 --- a/NEWS	Mon Dec 18 08:21:34 2006 +0100
     1.2 +++ b/NEWS	Mon Dec 18 08:21:35 2006 +0100
     1.3 @@ -553,10 +553,10 @@
     1.4  property, add the corresponding classes.
     1.5  
     1.6  * Locale Lattic_Locales.partial_order changed (to achieve consistency with
     1.7 -  axclass order):
     1.8 -  - moved to Orderings.partial_order
     1.9 -  - additional parameter ``less''
    1.10 -  INCOMPATIBILITY.
    1.11 +axclass order):
    1.12 +- moved to Orderings.partial_order
    1.13 +- additional parameter ``less''
    1.14 +INCOMPATIBILITY.
    1.15  
    1.16  * Constant "List.list_all2" in List.thy now uses authentic syntax.
    1.17  INCOMPATIBILITY: translations containing list_all2 may go wrong. On Isar
    1.18 @@ -768,6 +768,10 @@
    1.19  
    1.20  *** ML ***
    1.21  
    1.22 +* Pure/Isar/args.ML & Pure/Isar/method.ML
    1.23 +
    1.24 +switched argument order in *.syntax lifters.
    1.25 +
    1.26  * Pure/table:
    1.27  
    1.28  Function `...tab.foldl` removed.
     2.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Dec 18 08:21:34 2006 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Dec 18 08:21:35 2006 +0100
     2.3 @@ -154,7 +154,7 @@
     2.4    Method.syntax
     2.5     (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
     2.6      avoiding -- fixing -- rule_spec) src
     2.7 -  #> (fn (ctxt, (((x, y), z), w)) =>
     2.8 +  #> (fn ((((x, y), z), w), ctxt) =>
     2.9      Method.RAW_METHOD_CASES (fn facts =>
    2.10        HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
    2.11  
     3.1 --- a/src/HOL/Tools/function_package/auto_term.ML	Mon Dec 18 08:21:34 2006 +0100
     3.2 +++ b/src/HOL/Tools/function_package/auto_term.ML	Mon Dec 18 08:21:35 2006 +0100
     3.3 @@ -29,7 +29,7 @@
     3.4  
     3.5  
     3.6  val setup = Method.add_methods
     3.7 -  [("relation", (Method.SIMPLE_METHOD' o uncurry relation_tac) oo (Method.syntax Args.term),
     3.8 +  [("relation", (Method.SIMPLE_METHOD' o (fn (rel, ctxt) => relation_tac ctxt rel)) oo (Method.syntax Args.term),
     3.9      "proves termination using a user-specified wellfounded relation")]
    3.10  
    3.11  end
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Dec 18 08:21:34 2006 +0100
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Dec 18 08:21:35 2006 +0100
     4.3 @@ -440,7 +440,7 @@
     4.4  
     4.5  fun ind_cases src =
     4.6    Method.syntax (Scan.repeat1 Args.prop) src
     4.7 -  #> (fn (ctxt, props) => Method.erule 0 (map (mk_cases ctxt) props));
     4.8 +  #> (fn (props, ctxt) => Method.erule 0 (map (mk_cases ctxt) props));
     4.9  
    4.10  
    4.11  
     5.1 --- a/src/HOL/Tools/old_inductive_package.ML	Mon Dec 18 08:21:34 2006 +0100
     5.2 +++ b/src/HOL/Tools/old_inductive_package.ML	Mon Dec 18 08:21:35 2006 +0100
     5.3 @@ -583,7 +583,7 @@
     5.4  
     5.5  (* mk_cases_meth *)
     5.6  
     5.7 -fun mk_cases_meth (ctxt, raw_props) =
     5.8 +fun mk_cases_meth (raw_props, ctxt) =
     5.9    let
    5.10      val thy = ProofContext.theory_of ctxt;
    5.11      val ss = local_simpset_of ctxt;
     6.1 --- a/src/HOL/arith_data.ML	Mon Dec 18 08:21:34 2006 +0100
     6.2 +++ b/src/HOL/arith_data.ML	Mon Dec 18 08:21:35 2006 +0100
     6.3 @@ -1088,7 +1088,7 @@
     6.4      addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
     6.5      addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
     6.6    Method.add_methods
     6.7 -    [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
     6.8 +    [("arith", (arith_method o fst) oo Method.syntax Args.bang_facts,
     6.9        "decide linear arithmethic")] #>
    6.10    Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
    6.11      "declaration of split rules for arithmetic procedure")];
     7.1 --- a/src/HOL/ex/Reflection.thy	Mon Dec 18 08:21:34 2006 +0100
     7.2 +++ b/src/HOL/ex/Reflection.thy	Mon Dec 18 08:21:35 2006 +0100
     7.3 @@ -18,14 +18,14 @@
     7.4    fn src =>
     7.5      Method.syntax (Attrib.thms --
     7.6        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
     7.7 -  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
     7.8 +  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
     7.9  *} "partial automatic reification"
    7.10  
    7.11  method_setup reflection = {*
    7.12    fn src =>
    7.13      Method.syntax (Attrib.thms --
    7.14        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    7.15 -  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    7.16 +  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    7.17  *} "reflection method"
    7.18  
    7.19  end
     8.1 --- a/src/Provers/eqsubst.ML	Mon Dec 18 08:21:34 2006 +0100
     8.2 +++ b/src/Provers/eqsubst.ML	Mon Dec 18 08:21:35 2006 +0100
     8.3 @@ -538,7 +538,7 @@
     8.4  the goal) as well as the theorems to use *)
     8.5  fun subst_meth src =
     8.6    Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
     8.7 -  #> (fn (ctxt, ((asmflag, occL), inthms)) =>
     8.8 +  #> (fn (((asmflag, occL), inthms), ctxt) =>
     8.9      (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
    8.10  
    8.11  
     9.1 --- a/src/Provers/induct_method.ML	Mon Dec 18 08:21:34 2006 +0100
     9.2 +++ b/src/Provers/induct_method.ML	Mon Dec 18 08:21:35 2006 +0100
     9.3 @@ -517,7 +517,7 @@
     9.4  fun cases_meth src =
     9.5    Method.syntax (Args.mode openN --
     9.6      (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
     9.7 -  #> (fn (ctxt, (is_open, (insts, opt_rule))) =>
     9.8 +  #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
     9.9      Method.METHOD_CASES (fn facts =>
    9.10        Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
    9.11  
    9.12 @@ -525,14 +525,14 @@
    9.13    Method.syntax (Args.mode openN --
    9.14      (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
    9.15      (arbitrary -- taking -- Scan.option induct_rule))) src
    9.16 -  #> (fn (ctxt, (is_open, (insts, ((arbitrary, taking), opt_rule)))) =>
    9.17 +  #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
    9.18      Method.RAW_METHOD_CASES (fn facts =>
    9.19        Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
    9.20  
    9.21  fun coinduct_meth src =
    9.22    Method.syntax (Args.mode openN --
    9.23      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
    9.24 -  #> (fn (ctxt, (is_open, ((insts, taking), opt_rule))) =>
    9.25 +  #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
    9.26      Method.RAW_METHOD_CASES (fn facts =>
    9.27        Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
    9.28  
    10.1 --- a/src/Provers/splitter.ML	Mon Dec 18 08:21:34 2006 +0100
    10.2 +++ b/src/Provers/splitter.ML	Mon Dec 18 08:21:35 2006 +0100
    10.3 @@ -477,7 +477,7 @@
    10.4  
    10.5  fun split_meth src =
    10.6    Method.syntax Attrib.thms src
    10.7 -  #> (fn (_, ths) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
    10.8 +  #> (fn (ths, _) => Method.SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths));
    10.9  
   10.10  
   10.11  (* theory setup *)
    11.1 --- a/src/Pure/Isar/args.ML	Mon Dec 18 08:21:34 2006 +0100
    11.2 +++ b/src/Pure/Isar/args.ML	Mon Dec 18 08:21:35 2006 +0100
    11.3 @@ -84,9 +84,9 @@
    11.4      -> ((int -> tactic) -> tactic) * ('a * T list)
    11.5    val attribs: (string -> string) -> T list -> src list * T list
    11.6    val opt_attribs: (string -> string) -> T list -> src list * T list
    11.7 -  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'b * 'a
    11.8 +  val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
    11.9    val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
   11.10 -    src -> Proof.context -> Proof.context * 'a
   11.11 +    src -> Proof.context -> 'a * Proof.context
   11.12  end;
   11.13  
   11.14  structure Args: ARGS =
   11.15 @@ -393,11 +393,11 @@
   11.16  
   11.17  fun syntax kind scan (src as Src ((s, args), pos)) st =
   11.18    (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
   11.19 -    (SOME x, (st', [])) => (st', x)
   11.20 +    (SOME x, (st', [])) => (x, st')
   11.21    | (_, (_, args')) =>
   11.22        error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n  " ^
   11.23          space_implode " " (map string_of args')));
   11.24  
   11.25 -fun context_syntax kind scan src = apfst Context.the_proof o syntax kind scan src o Context.Proof;
   11.26 +fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
   11.27  
   11.28  end;
    12.1 --- a/src/Pure/Isar/attrib.ML	Mon Dec 18 08:21:34 2006 +0100
    12.2 +++ b/src/Pure/Isar/attrib.ML	Mon Dec 18 08:21:35 2006 +0100
    12.3 @@ -185,7 +185,7 @@
    12.4  (** attribute syntax **)
    12.5  
    12.6  fun syntax scan src (st, th) =
    12.7 -  let val (st', f) = Args.syntax "attribute" scan src st
    12.8 +  let val (f, st') = Args.syntax "attribute" scan src st
    12.9    in f (st', th) end;
   12.10  
   12.11  fun no_args x = syntax (Scan.succeed x);
    13.1 --- a/src/Pure/Isar/isar_output.ML	Mon Dec 18 08:21:34 2006 +0100
    13.2 +++ b/src/Pure/Isar/isar_output.ML	Mon Dec 18 08:21:35 2006 +0100
    13.3 @@ -115,7 +115,7 @@
    13.4  fun args scan f src node : string =
    13.5    let
    13.6      val loc = if ! locale = "" then NONE else SOME (! locale);
    13.7 -    val (ctxt, x) = syntax scan src (Toplevel.presentation_context node loc);
    13.8 +    val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
    13.9    in f src ctxt x end;
   13.10  
   13.11  
    14.1 --- a/src/Pure/Isar/method.ML	Mon Dec 18 08:21:34 2006 +0100
    14.2 +++ b/src/Pure/Isar/method.ML	Mon Dec 18 08:21:35 2006 +0100
    14.3 @@ -79,7 +79,7 @@
    14.4      -> theory -> theory
    14.5    val method_setup: bstring * string * string -> theory -> theory
    14.6    val syntax: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list))
    14.7 -    -> src -> Proof.context -> Proof.context * 'a
    14.8 +    -> src -> Proof.context -> 'a * Proof.context
    14.9    val simple_args: (Args.T list -> 'a * Args.T list)
   14.10      -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   14.11    val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
   14.12 @@ -459,10 +459,10 @@
   14.13  fun syntax scan = Args.context_syntax "method" scan;
   14.14  
   14.15  fun simple_args scan f src ctxt : method =
   14.16 -  #2 (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
   14.17 +  fst (syntax (Scan.lift (scan >> (fn x => f x ctxt))) src ctxt);
   14.18  
   14.19  fun ctxt_args (f: Proof.context -> method) src ctxt =
   14.20 -  #2 (syntax (Scan.succeed (f ctxt)) src ctxt);
   14.21 +  fst (syntax (Scan.succeed (f ctxt)) src ctxt);
   14.22  
   14.23  fun no_args m = ctxt_args (K m);
   14.24  
   14.25 @@ -486,7 +486,7 @@
   14.26  in
   14.27  
   14.28  fun sectioned_args args ss f src ctxt =
   14.29 -  let val (ctxt', (x, _)) = syntax (sectioned args ss) src ctxt
   14.30 +  let val ((x, _), ctxt') = syntax (sectioned args ss) src ctxt
   14.31    in f x ctxt' end;
   14.32  
   14.33  fun bang_sectioned_args ss f = sectioned_args Args.bang_facts ss f;
   14.34 @@ -537,15 +537,15 @@
   14.35  (* tactic syntax *)
   14.36  
   14.37  fun nat_thms_args f = uncurry f oo
   14.38 -  (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
   14.39 +  (fst oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
   14.40  
   14.41 -fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   14.42 +fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec HEADGOAL -- args >>
   14.43    (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
   14.44  
   14.45  fun goal_args args tac = goal_args' (Scan.lift args) tac;
   14.46  
   14.47  fun goal_args_ctxt' args tac src ctxt =
   14.48 -  #2 (syntax (Args.goal_spec HEADGOAL -- args >>
   14.49 +  fst (syntax (Args.goal_spec HEADGOAL -- args >>
   14.50    (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
   14.51  
   14.52  fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
   14.53 @@ -562,7 +562,7 @@
   14.54    ("elim", thms_args elim, "repeatedly apply elimination rules"),
   14.55    ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"),
   14.56    ("fold", thms_ctxt_args fold_meth, "fold definitions"),
   14.57 -  ("atomize", (atomize o #2) oo syntax (Args.mode "full"),
   14.58 +  ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
   14.59      "present local premises as object-level statements"),
   14.60    ("iprover", iprover_meth, "intuitionistic proof search"),
   14.61    ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
    15.1 --- a/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:34 2006 +0100
    15.2 +++ b/src/Pure/Isar/rule_insts.ML	Mon Dec 18 08:21:35 2006 +0100
    15.3 @@ -349,7 +349,7 @@
    15.4        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
    15.5  
    15.6  fun inst_args f src ctxt =
    15.7 -  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    15.8 +  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
    15.9  
   15.10  val insts_var =
   15.11    Scan.optional
   15.12 @@ -357,7 +357,7 @@
   15.13        Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   15.14  
   15.15  fun inst_args_var f src ctxt =
   15.16 -  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
   15.17 +  f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
   15.18  
   15.19  
   15.20  (* setup *)
    16.1 --- a/src/ZF/Tools/ind_cases.ML	Mon Dec 18 08:21:34 2006 +0100
    16.2 +++ b/src/ZF/Tools/ind_cases.ML	Mon Dec 18 08:21:35 2006 +0100
    16.3 @@ -60,7 +60,7 @@
    16.4  
    16.5  (* ind_cases method *)
    16.6  
    16.7 -fun mk_cases_meth (ctxt, props) =
    16.8 +fun mk_cases_meth (props, ctxt) =
    16.9    props
   16.10    |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
   16.11      (ProofContext.read_prop ctxt))