# HG changeset patch
# User wenzelm
# Date 1377270072 -7200
# Node ID d998de7f0efccf94e741a02f590259587ae0ad3c
# Parent  4e7ddd76e632b20f528f664a30d6a1cbbbfb108f
tuned signature;

diff -r 4e7ddd76e632 -r d998de7f0efc src/HOL/Decision_Procs/Cooper.thy
--- 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"
 
diff -r 4e7ddd76e632 -r d998de7f0efc src/HOL/Decision_Procs/Ferrack.thy
--- 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"
 
diff -r 4e7ddd76e632 -r d998de7f0efc src/HOL/Decision_Procs/MIR.thy
--- 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"
 
diff -r 4e7ddd76e632 -r d998de7f0efc src/HOL/Nominal/nominal_induct.ML
--- 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)));
diff -r 4e7ddd76e632 -r d998de7f0efc src/Pure/Isar/args.ML
--- 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;
diff -r 4e7ddd76e632 -r d998de7f0efc src/Pure/Isar/attrib.ML
--- 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" #>
diff -r 4e7ddd76e632 -r d998de7f0efc src/Pure/Isar/method.ML
--- 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)" #>
diff -r 4e7ddd76e632 -r d998de7f0efc src/Pure/ML/ml_thms.ML
--- 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;
diff -r 4e7ddd76e632 -r d998de7f0efc src/Tools/eqsubst.ML
--- 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)))
diff -r 4e7ddd76e632 -r d998de7f0efc src/Tools/induct.ML
--- 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