--- a/src/HOL/Decision_Procs/Cooper.thy Fri Aug 23 15:36:54 2013 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy Fri Aug 23 17:01:12 2013 +0200
@@ -2140,7 +2140,7 @@
ML_file "cooper_tac.ML"
method_setup cooper = {*
- Args.mode "no_quantify" >>
+ Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Cooper_Tac.linz_tac ctxt (not q)))
*} "decision procedure for linear integer arithmetic"
--- a/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 23 15:36:54 2013 +0200
+++ b/src/HOL/Decision_Procs/Ferrack.thy Fri Aug 23 17:01:12 2013 +0200
@@ -2009,7 +2009,7 @@
ML_file "ferrack_tac.ML"
method_setup rferrack = {*
- Args.mode "no_quantify" >>
+ Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Ferrack_Tac.linr_tac ctxt (not q)))
*} "decision procedure for linear real arithmetic"
--- a/src/HOL/Decision_Procs/MIR.thy Fri Aug 23 15:36:54 2013 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Aug 23 17:01:12 2013 +0200
@@ -5665,7 +5665,7 @@
ML_file "mir_tac.ML"
method_setup mir = {*
- Args.mode "no_quantify" >>
+ Scan.lift (Args.mode "no_quantify") >>
(fn q => fn ctxt => SIMPLE_METHOD' (Mir_Tac.mir_tac ctxt (not q)))
*} "decision procedure for MIR arithmetic"
--- a/src/HOL/Nominal/nominal_induct.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Aug 23 17:01:12 2013 +0200
@@ -169,8 +169,9 @@
in
val nominal_induct_method =
- Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
- avoiding -- fixing -- rule_spec) >>
+ Scan.lift (Args.mode Induct.no_simpN) --
+ (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ avoiding -- fixing -- rule_spec) >>
(fn (no_simp, (((x, y), z), w)) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
--- a/src/Pure/Isar/args.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Pure/Isar/args.ML Fri Aug 23 17:01:12 2013 +0200
@@ -25,9 +25,9 @@
val bang: string parser
val query_colon: string parser
val bang_colon: string parser
- val parens: ('a parser) -> 'a parser
- val bracks: ('a parser) -> 'a parser
- val mode: string -> bool context_parser
+ val parens: 'a parser -> 'a parser
+ val bracks: 'a parser -> 'a parser
+ val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
val name_source: string parser
val name_source_position: (Symbol_Pos.text * Position.T) parser
@@ -145,7 +145,7 @@
fun parens scan = $$$ "(" |-- scan --| $$$ ")";
fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
-fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
+fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
val name_source = named >> Token.source_of;
--- a/src/Pure/Isar/attrib.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Pure/Isar/attrib.ML Fri Aug 23 17:01:12 2013 +0200
@@ -353,8 +353,8 @@
(* rule format *)
-val rule_format = Args.mode "no_asm"
- >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
+fun rule_format true = Object_Logic.rule_format_no_asm
+ | rule_format false = Object_Logic.rule_format;
val elim_format = Thm.rule_attribute (K Tactic.make_elim);
@@ -410,7 +410,8 @@
"named rule parameters" #>
setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
"result put into standard form (legacy)" #>
- setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
+ setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
+ "result put into canonical rule format" #>
setup (Binding.name "elim_format") (Scan.succeed elim_format)
"destruct rule turned into elimination rule format" #>
setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
--- a/src/Pure/Isar/method.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Pure/Isar/method.ML Fri Aug 23 17:01:12 2013 +0200
@@ -451,7 +451,7 @@
"repeatedly apply elimination rules" #>
setup (Binding.name "unfold") (Attrib.thms >> unfold_meth) "unfold definitions" #>
setup (Binding.name "fold") (Attrib.thms >> fold_meth) "fold definitions" #>
- setup (Binding.name "atomize") (Args.mode "full" >> (K o atomize))
+ setup (Binding.name "atomize") (Scan.lift (Args.mode "full") >> (K o atomize))
"present local premises as object-level statements" #>
setup (Binding.name "rule") (Attrib.thms >> some_rule) "apply some intro/elim rule" #>
setup (Binding.name "erule") (xrule_meth erule) "apply rule in elimination manner (improper)" #>
--- a/src/Pure/ML/ml_thms.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Pure/ML/ml_thms.ML Fri Aug 23 17:01:12 2013 +0200
@@ -85,10 +85,10 @@
val _ =
Context.>> (Context.map_theory
(ML_Context.add_antiq (Binding.name "lemma")
- (fn _ => Args.context -- Args.mode "open" --
- Scan.lift (Parse.and_list1 (Scan.repeat1 goal) --
+ (fn _ => Args.context --
+ Scan.lift (Args.mode "open" -- Parse.and_list1 (Scan.repeat1 goal) --
(by |-- Method.parse -- Scan.option Method.parse)) >>
- (fn ((ctxt, is_open), (raw_propss, methods)) =>
+ (fn (ctxt, ((is_open, raw_propss), methods)) =>
let
val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss;
val prep_result = Goal.norm_result #> not is_open ? Thm.close_derivation;
--- a/src/Tools/eqsubst.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Tools/eqsubst.ML Fri Aug 23 17:01:12 2013 +0200
@@ -420,7 +420,7 @@
the goal) as well as the theorems to use *)
val setup =
Method.setup @{binding subst}
- (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
+ (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
Attrib.thms >>
(fn ((asm, occs), inthms) => fn ctxt =>
SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
--- a/src/Tools/induct.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/Tools/induct.ML Fri Aug 23 17:01:12 2013 +0200
@@ -919,7 +919,7 @@
val cases_setup =
Method.setup @{binding cases}
- (Args.mode no_simpN --
+ (Scan.lift (Args.mode no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
(fn (no_simp, (insts, opt_rule)) => fn ctxt =>
METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
@@ -928,8 +928,9 @@
fun gen_induct_setup binding itac =
Method.setup binding
- (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
- (arbitrary -- taking -- Scan.option induct_rule)) >>
+ (Scan.lift (Args.mode no_simpN) --
+ (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
+ (arbitrary -- taking -- Scan.option induct_rule)) >>
(fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
RAW_METHOD_CASES (fn facts =>
Seq.DETERM