tuned signature;
authorwenzelm
Fri Aug 23 17:01:12 2013 +0200 (2013-08-23)
changeset 53168d998de7f0efc
parent 53167 4e7ddd76e632
child 53169 e2d31807cbf6
tuned signature;
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/MIR.thy
src/HOL/Nominal/nominal_induct.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_thms.ML
src/Tools/eqsubst.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 23 15:36:54 2013 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Aug 23 17:01:12 2013 +0200
     1.3 @@ -2140,7 +2140,7 @@
     1.4  ML_file "cooper_tac.ML"
     1.5  
     1.6  method_setup cooper = {*
     1.7 -  Args.mode "no_quantify" >>
     1.8 +  Scan.lift (Args.mode "no_quantify") >>
     1.9      (fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
    1.10  *} "decision procedure for linear integer arithmetic"
    1.11  
     2.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 23 15:36:54 2013 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Fri Aug 23 17:01:12 2013 +0200
     2.3 @@ -2009,7 +2009,7 @@
     2.4  ML_file "ferrack_tac.ML"
     2.5  
     2.6  method_setup rferrack = {*
     2.7 -  Args.mode "no_quantify" >>
     2.8 +  Scan.lift (Args.mode "no_quantify") >>
     2.9      (fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
    2.10  *} "decision procedure for linear real arithmetic"
    2.11  
     3.1 --- a/src/HOL/Decision_Procs/MIR.thy	Fri Aug 23 15:36:54 2013 +0200
     3.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Fri Aug 23 17:01:12 2013 +0200
     3.3 @@ -5665,7 +5665,7 @@
     3.4  ML_file "mir_tac.ML"
     3.5  
     3.6  method_setup mir = {*
     3.7 -  Args.mode "no_quantify" >>
     3.8 +  Scan.lift (Args.mode "no_quantify") >>
     3.9      (fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
    3.10  *} "decision procedure for MIR arithmetic"
    3.11  
     4.1 --- a/src/HOL/Nominal/nominal_induct.ML	Fri Aug 23 15:36:54 2013 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Fri Aug 23 17:01:12 2013 +0200
     4.3 @@ -169,8 +169,9 @@
     4.4  in
     4.5  
     4.6  val nominal_induct_method =
     4.7 -  Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
     4.8 -  avoiding -- fixing -- rule_spec) >>
     4.9 +  Scan.lift (Args.mode Induct.no_simpN) --
    4.10 +  (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    4.11 +    avoiding -- fixing -- rule_spec) >>
    4.12    (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
    4.13      RAW_METHOD_CASES (fn facts =>
    4.14        HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
     5.1 --- a/src/Pure/Isar/args.ML	Fri Aug 23 15:36:54 2013 +0200
     5.2 +++ b/src/Pure/Isar/args.ML	Fri Aug 23 17:01:12 2013 +0200
     5.3 @@ -25,9 +25,9 @@
     5.4    val bang: string parser
     5.5    val query_colon: string parser
     5.6    val bang_colon: string parser
     5.7 -  val parens: ('a parser) -> 'a parser
     5.8 -  val bracks: ('a parser) -> 'a parser
     5.9 -  val mode: string -> bool context_parser
    5.10 +  val parens: 'a parser -> 'a parser
    5.11 +  val bracks: 'a parser -> 'a parser
    5.12 +  val mode: string -> bool parser
    5.13    val maybe: 'a parser -> 'a option parser
    5.14    val name_source: string parser
    5.15    val name_source_position: (Symbol_Pos.text * Position.T) parser
    5.16 @@ -145,7 +145,7 @@
    5.17  
    5.18  fun parens scan = $$$ "(" |-- scan --| $$$ ")";
    5.19  fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
    5.20 -fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
    5.21 +fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
    5.22  fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
    5.23  
    5.24  val name_source = named >> Token.source_of;
     6.1 --- a/src/Pure/Isar/attrib.ML	Fri Aug 23 15:36:54 2013 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Fri Aug 23 17:01:12 2013 +0200
     6.3 @@ -353,8 +353,8 @@
     6.4  
     6.5  (* rule format *)
     6.6  
     6.7 -val rule_format = Args.mode "no_asm"
     6.8 -  >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
     6.9 +fun rule_format true = Object_Logic.rule_format_no_asm
    6.10 +  | rule_format false = Object_Logic.rule_format;
    6.11  
    6.12  val elim_format = Thm.rule_attribute (K Tactic.make_elim);
    6.13  
    6.14 @@ -410,7 +410,8 @@
    6.15      "named rule parameters" #>
    6.16    setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
    6.17      "result put into standard form (legacy)" #>
    6.18 -  setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
    6.19 +  setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
    6.20 +    "result put into canonical rule format" #>
    6.21    setup (Binding.name "elim_format") (Scan.succeed elim_format)
    6.22      "destruct rule turned into elimination rule format" #>
    6.23    setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
     7.1 --- a/src/Pure/Isar/method.ML	Fri Aug 23 15:36:54 2013 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Fri Aug 23 17:01:12 2013 +0200
     7.3 @@ -451,7 +451,7 @@
     7.4      "repeatedly apply elimination rules" #>
     7.5    setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
     7.6    setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
     7.7 -  setup (Binding.name "atomize") (Args.mode "full" >> (K o atomize))
     7.8 +  setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
     7.9      "present local premises as object-level statements" #>
    7.10    setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
    7.11    setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
     8.1 --- a/src/Pure/ML/ml_thms.ML	Fri Aug 23 15:36:54 2013 +0200
     8.2 +++ b/src/Pure/ML/ml_thms.ML	Fri Aug 23 17:01:12 2013 +0200
     8.3 @@ -85,10 +85,10 @@
     8.4  val _ =
     8.5    Context.>> (Context.map_theory
     8.6     (ML_Context.add_antiq (Binding.name "lemma")
     8.7 -    (fn _ => Args.context -- Args.mode "open" --
     8.8 -        Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
     8.9 +    (fn _ => Args.context --
    8.10 +        Scan.lift (Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
    8.11            (by |-- Method.parse -- Scan.option Method.parse)) >>
    8.12 -      (fn ((ctxt, is_open), (raw_propss, methods)) =>
    8.13 +      (fn (ctxt, ((is_open, raw_propss), methods)) =>
    8.14          let
    8.15            val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
    8.16            val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
     9.1 --- a/src/Tools/eqsubst.ML	Fri Aug 23 15:36:54 2013 +0200
     9.2 +++ b/src/Tools/eqsubst.ML	Fri Aug 23 17:01:12 2013 +0200
     9.3 @@ -420,7 +420,7 @@
     9.4     the goal) as well as the theorems to use *)
     9.5  val setup =
     9.6    Method.setup @{binding subst}
     9.7 -    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
     9.8 +    (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
     9.9          Attrib.thms >>
    9.10        (fn ((asm, occs), inthms) => fn ctxt =>
    9.11          SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
    10.1 --- a/src/Tools/induct.ML	Fri Aug 23 15:36:54 2013 +0200
    10.2 +++ b/src/Tools/induct.ML	Fri Aug 23 17:01:12 2013 +0200
    10.3 @@ -919,7 +919,7 @@
    10.4  
    10.5  val cases_setup =
    10.6    Method.setup @{binding cases}
    10.7 -    (Args.mode no_simpN --
    10.8 +    (Scan.lift (Args.mode no_simpN) --
    10.9        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
   10.10        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
   10.11          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
   10.12 @@ -928,8 +928,9 @@
   10.13  
   10.14  fun gen_induct_setup binding itac =
   10.15    Method.setup binding
   10.16 -    (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   10.17 -      (arbitrary -- taking -- Scan.option induct_rule)) >>
   10.18 +    (Scan.lift (Args.mode no_simpN) --
   10.19 +      (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
   10.20 +        (arbitrary -- taking -- Scan.option induct_rule)) >>
   10.21        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
   10.22          RAW_METHOD_CASES (fn facts =>
   10.23            Seq.DETERM