simplified method setup;
authorwenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549d2d7874648bd
parent 30548 2eef5e71edd6
child 30550 c601204b055c
simplified method setup;
src/Cube/Example.thy
src/FOL/FOL.thy
src/FOL/ex/Iff_Oracle.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/OtwayReesBella.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Code_Setup.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Groebner_Basis.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/HoareParallel/OG_Tactics.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Reflection.thy
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Presburger.thy
src/HOL/Prolog/HOHH.thy
src/HOL/SAT.thy
src/HOL/SET-Protocol/Cardholder_Registration.thy
src/HOL/SET-Protocol/EventSET.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/SET-Protocol/Purchase.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/Word/WordArith.thy
src/HOL/ex/Binary.thy
src/HOL/ex/SAT_Examples.thy
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/Sequents/S4.thy
src/Sequents/S43.thy
src/Sequents/T.thy
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/Cube/Example.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/Cube/Example.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -15,20 +15,19 @@
     1.4  *}
     1.5  
     1.6  method_setup depth_solve = {*
     1.7 -  Method.thms_args (fn thms => METHOD (fn facts =>
     1.8 -  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
     1.9 +  Attrib.thms >> (fn thms => K (METHOD (fn facts =>
    1.10 +  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
    1.11  *} ""
    1.12  
    1.13  method_setup depth_solve1 = {*
    1.14 -  Method.thms_args (fn thms => METHOD (fn facts =>
    1.15 -  (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
    1.16 +  Attrib.thms >> (fn thms => K (METHOD (fn facts =>
    1.17 +  (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
    1.18  *} ""
    1.19  
    1.20  method_setup strip_asms =  {*
    1.21 -  let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
    1.22 -    Method.thms_args (fn thms => METHOD (fn facts =>
    1.23 -      REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
    1.24 -  end
    1.25 +  Attrib.thms >> (fn thms => K (METHOD (fn facts =>
    1.26 +    REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
    1.27 +    DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
    1.28  *} ""
    1.29  
    1.30  
     2.1 --- a/src/FOL/FOL.thy	Mon Mar 16 17:51:24 2009 +0100
     2.2 +++ b/src/FOL/FOL.thy	Mon Mar 16 18:24:30 2009 +0100
     2.3 @@ -73,9 +73,10 @@
     2.4    fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
     2.5  *}
     2.6  
     2.7 -method_setup case_tac =
     2.8 -  {* Method.goal_args_ctxt Args.name_source case_tac *}
     2.9 -  "case_tac emulation (dynamic instantiation!)"
    2.10 +method_setup case_tac = {*
    2.11 +  Args.goal_spec -- Scan.lift Args.name_source >>
    2.12 +  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
    2.13 +*} "case_tac emulation (dynamic instantiation!)"
    2.14  
    2.15  
    2.16  (*** Special elimination rules *)
     3.1 --- a/src/FOL/ex/Iff_Oracle.thy	Mon Mar 16 17:51:24 2009 +0100
     3.2 +++ b/src/FOL/ex/Iff_Oracle.thy	Mon Mar 16 18:24:30 2009 +0100
     3.3 @@ -52,7 +52,7 @@
     3.4  subsection {* Oracle as proof method *}
     3.5  
     3.6  method_setup iff = {*
     3.7 -  Method.simple_args OuterParse.nat (fn n => fn ctxt =>
     3.8 +  Scan.lift OuterParse.nat >> (fn n => fn ctxt =>
     3.9      SIMPLE_METHOD
    3.10        (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
    3.11          handle Fail _ => no_tac))
     4.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Mar 16 17:51:24 2009 +0100
     4.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Mar 16 18:24:30 2009 +0100
     4.3 @@ -222,7 +222,7 @@
     4.4  *}   (* Note: r_one is not necessary in ring_ss *)
     4.5  
     4.6  method_setup ring =
     4.7 -  {* Method.no_args (SIMPLE_METHOD' (full_simp_tac ring_ss)) *}
     4.8 +  {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
     4.9    {* computes distributive normal form in rings *}
    4.10  
    4.11  
     5.1 --- a/src/HOL/Auth/Event.thy	Mon Mar 16 17:51:24 2009 +0100
     5.2 +++ b/src/HOL/Auth/Event.thy	Mon Mar 16 18:24:30 2009 +0100
     5.3 @@ -289,7 +289,7 @@
     5.4  *}
     5.5  
     5.6  method_setup analz_mono_contra = {*
     5.7 -    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
     5.8 +    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
     5.9      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
    5.10  
    5.11  subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
    5.12 @@ -310,7 +310,7 @@
    5.13  *}
    5.14  
    5.15  method_setup synth_analz_mono_contra = {*
    5.16 -    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac)) *}
    5.17 +    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST synth_analz_mono_contra_tac))) *}
    5.18      "for proving theorems of the form X \<notin> synth (analz (knows Spy evs)) --> P"
    5.19  
    5.20  end
     6.1 --- a/src/HOL/Auth/Message.thy	Mon Mar 16 17:51:24 2009 +0100
     6.2 +++ b/src/HOL/Auth/Message.thy	Mon Mar 16 18:24:30 2009 +0100
     6.3 @@ -941,15 +941,15 @@
     6.4  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
     6.5  
     6.6  method_setup spy_analz = {*
     6.7 -    Method.ctxt_args (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
     6.8 +    Scan.succeed (SIMPLE_METHOD' o Message.gen_spy_analz_tac o local_clasimpset_of) *}
     6.9      "for proving the Fake case when analz is involved"
    6.10  
    6.11  method_setup atomic_spy_analz = {*
    6.12 -    Method.ctxt_args (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
    6.13 +    Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
    6.14      "for debugging spy_analz"
    6.15  
    6.16  method_setup Fake_insert_simp = {*
    6.17 -    Method.ctxt_args (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
    6.18 +    Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
    6.19      "for debugging spy_analz"
    6.20  
    6.21  end
     7.1 --- a/src/HOL/Auth/OtwayReesBella.thy	Mon Mar 16 17:51:24 2009 +0100
     7.2 +++ b/src/HOL/Auth/OtwayReesBella.thy	Mon Mar 16 18:24:30 2009 +0100
     7.3 @@ -137,7 +137,7 @@
     7.4  *}
     7.5   
     7.6  method_setup parts_explicit = {*
     7.7 -    Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
     7.8 +    Scan.succeed (K (SIMPLE_METHOD' parts_explicit_tac)) *}
     7.9    "to explicitly state that some message components belong to parts knows Spy"
    7.10  
    7.11  
    7.12 @@ -257,7 +257,7 @@
    7.13  *}
    7.14  
    7.15  method_setup analz_freshCryptK = {*
    7.16 -    Method.ctxt_args (fn ctxt =>
    7.17 +    Scan.succeed (fn ctxt =>
    7.18       (SIMPLE_METHOD
    7.19        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    7.20            REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
    7.21 @@ -267,10 +267,10 @@
    7.22  
    7.23  
    7.24  method_setup disentangle = {*
    7.25 -    Method.no_args
    7.26 -     (SIMPLE_METHOD
    7.27 +    Scan.succeed
    7.28 +     (K (SIMPLE_METHOD
    7.29        (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] 
    7.30 -                   ORELSE' hyp_subst_tac))) *}
    7.31 +                   ORELSE' hyp_subst_tac)))) *}
    7.32    "for eliminating conjunctions, disjunctions and the like"
    7.33  
    7.34  
     8.1 --- a/src/HOL/Auth/Public.thy	Mon Mar 16 17:51:24 2009 +0100
     8.2 +++ b/src/HOL/Auth/Public.thy	Mon Mar 16 18:24:30 2009 +0100
     8.3 @@ -424,7 +424,7 @@
     8.4  *}
     8.5  
     8.6  method_setup analz_freshK = {*
     8.7 -    Method.ctxt_args (fn ctxt =>
     8.8 +    Scan.succeed (fn ctxt =>
     8.9       (SIMPLE_METHOD
    8.10        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    8.11            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    8.12 @@ -435,11 +435,11 @@
    8.13  subsection{*Specialized Methods for Possibility Theorems*}
    8.14  
    8.15  method_setup possibility = {*
    8.16 -    Method.ctxt_args (SIMPLE_METHOD o Public.possibility_tac) *}
    8.17 +    Scan.succeed (SIMPLE_METHOD o Public.possibility_tac) *}
    8.18      "for proving possibility theorems"
    8.19  
    8.20  method_setup basic_possibility = {*
    8.21 -    Method.ctxt_args (SIMPLE_METHOD o Public.basic_possibility_tac) *}
    8.22 +    Scan.succeed (SIMPLE_METHOD o Public.basic_possibility_tac) *}
    8.23      "for proving possibility theorems"
    8.24  
    8.25  end
     9.1 --- a/src/HOL/Auth/Shared.thy	Mon Mar 16 17:51:24 2009 +0100
     9.2 +++ b/src/HOL/Auth/Shared.thy	Mon Mar 16 18:24:30 2009 +0100
     9.3 @@ -238,7 +238,7 @@
     9.4  (*Specialized methods*)
     9.5  
     9.6  method_setup analz_freshK = {*
     9.7 -    Method.ctxt_args (fn ctxt =>
     9.8 +    Scan.succeed (fn ctxt =>
     9.9       (SIMPLE_METHOD
    9.10        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
    9.11            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    9.12 @@ -246,11 +246,11 @@
    9.13      "for proving the Session Key Compromise theorem"
    9.14  
    9.15  method_setup possibility = {*
    9.16 -    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
    9.17 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.possibility_tac ctxt)) *}
    9.18      "for proving possibility theorems"
    9.19  
    9.20  method_setup basic_possibility = {*
    9.21 -    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
    9.22 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *}
    9.23      "for proving possibility theorems"
    9.24  
    9.25  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
    10.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Mon Mar 16 17:51:24 2009 +0100
    10.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Mon Mar 16 18:24:30 2009 +0100
    10.3 @@ -769,15 +769,15 @@
    10.4  *}
    10.5  
    10.6  method_setup prepare = {*
    10.7 -    Method.no_args (SIMPLE_METHOD ShoupRubin.prepare_tac) *}
    10.8 +    Scan.succeed (K (SIMPLE_METHOD ShoupRubin.prepare_tac)) *}
    10.9    "to launch a few simple facts that'll help the simplifier"
   10.10  
   10.11  method_setup parts_prepare = {*
   10.12 -    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
   10.13 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *}
   10.14    "additional facts to reason about parts"
   10.15  
   10.16  method_setup analz_prepare = {*
   10.17 -    Method.no_args (SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *}
   10.18 +    Scan.succeed (K (SIMPLE_METHOD ShoupRubin.analz_prepare_tac)) *}
   10.19    "additional facts to reason about analz"
   10.20  
   10.21  
   10.22 @@ -822,7 +822,7 @@
   10.23  done
   10.24  
   10.25  method_setup sc_analz_freshK = {*
   10.26 -    Method.ctxt_args (fn ctxt =>
   10.27 +    Scan.succeed (fn ctxt =>
   10.28       (SIMPLE_METHOD
   10.29        (EVERY [REPEAT_FIRST
   10.30         (resolve_tac [allI, ballI, impI]),
    11.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Mon Mar 16 17:51:24 2009 +0100
    11.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Mon Mar 16 18:24:30 2009 +0100
    11.3 @@ -777,15 +777,15 @@
    11.4  *}
    11.5  
    11.6  method_setup prepare = {*
    11.7 -    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
    11.8 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
    11.9    "to launch a few simple facts that'll help the simplifier"
   11.10  
   11.11  method_setup parts_prepare = {*
   11.12 -    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   11.13 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
   11.14    "additional facts to reason about parts"
   11.15  
   11.16  method_setup analz_prepare = {*
   11.17 -    Method.ctxt_args (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   11.18 +    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
   11.19    "additional facts to reason about analz"
   11.20  
   11.21  
   11.22 @@ -831,7 +831,7 @@
   11.23  done
   11.24  
   11.25  method_setup sc_analz_freshK = {*
   11.26 -    Method.ctxt_args (fn ctxt =>
   11.27 +    Scan.succeed (fn ctxt =>
   11.28       (SIMPLE_METHOD
   11.29        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   11.30            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
    12.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Mar 16 17:51:24 2009 +0100
    12.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Mar 16 18:24:30 2009 +0100
    12.3 @@ -407,7 +407,7 @@
    12.4  (*Specialized methods*)
    12.5  
    12.6  method_setup analz_freshK = {*
    12.7 -    Method.ctxt_args (fn ctxt =>
    12.8 +    Scan.succeed (fn ctxt =>
    12.9       (SIMPLE_METHOD
   12.10        (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
   12.11            REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
   12.12 @@ -415,12 +415,12 @@
   12.13      "for proving the Session Key Compromise theorem"
   12.14  
   12.15  method_setup possibility = {*
   12.16 -    Method.ctxt_args (fn ctxt =>
   12.17 +    Scan.succeed (fn ctxt =>
   12.18          SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *}
   12.19      "for proving possibility theorems"
   12.20  
   12.21  method_setup basic_possibility = {*
   12.22 -    Method.ctxt_args (fn ctxt =>
   12.23 +    Scan.succeed (fn ctxt =>
   12.24          SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *}
   12.25      "for proving possibility theorems"
   12.26  
    13.1 --- a/src/HOL/Code_Setup.thy	Mon Mar 16 17:51:24 2009 +0100
    13.2 +++ b/src/HOL/Code_Setup.thy	Mon Mar 16 18:24:30 2009 +0100
    13.3 @@ -226,19 +226,19 @@
    13.4  *}
    13.5  
    13.6  ML {*
    13.7 -fun gen_eval_method conv = Method.ctxt_args (fn ctxt => SIMPLE_METHOD'
    13.8 +fun gen_eval_method conv ctxt = SIMPLE_METHOD'
    13.9    (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   13.10 -    THEN' rtac TrueI))
   13.11 +    THEN' rtac TrueI)
   13.12  *}
   13.13  
   13.14 -method_setup eval = {* gen_eval_method eval_oracle *}
   13.15 +method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
   13.16    "solve goal by evaluation"
   13.17  
   13.18 -method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
   13.19 +method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   13.20    "solve goal by evaluation"
   13.21  
   13.22 -method_setup normalization = {* (Method.no_args o SIMPLE_METHOD')
   13.23 -  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
   13.24 +method_setup normalization = {*
   13.25 +  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
   13.26  *} "solve goal by normalization"
   13.27  
   13.28  
    14.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 16 17:51:24 2009 +0100
    14.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Mar 16 18:24:30 2009 +0100
    14.3 @@ -2496,16 +2496,15 @@
    14.4  
    14.5  *}
    14.6  
    14.7 -method_setup approximation = {* fn src => 
    14.8 -  Method.syntax Args.term src #>
    14.9 -  (fn (prec, ctxt) => let
   14.10 -   in SIMPLE_METHOD' (fn i =>
   14.11 +method_setup approximation = {*
   14.12 +  Args.term >>
   14.13 +  (fn prec => fn ctxt =>
   14.14 +    SIMPLE_METHOD' (fn i =>
   14.15       (DETERM (reify_uneq ctxt i)
   14.16        THEN rule_uneq ctxt prec i
   14.17        THEN Simplifier.asm_full_simp_tac bounded_by_simpset i 
   14.18        THEN (TRY (filter_prems_tac (fn t => false) i))
   14.19 -      THEN (gen_eval_tac eval_oracle ctxt) i))
   14.20 -   end)
   14.21 +      THEN (gen_eval_tac eval_oracle ctxt) i)))
   14.22  *} "real number approximation"
   14.23   
   14.24  end
    15.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Mar 16 17:51:24 2009 +0100
    15.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Mon Mar 16 18:24:30 2009 +0100
    15.3 @@ -295,7 +295,7 @@
    15.4  
    15.5  use "~~/src/HOL/Tools/Qelim/langford.ML"
    15.6  method_setup dlo = {*
    15.7 -  Method.ctxt_args (SIMPLE_METHOD' o LangfordQE.dlo_tac)
    15.8 +  Scan.succeed (SIMPLE_METHOD' o LangfordQE.dlo_tac)
    15.9  *} "Langford's algorithm for quantifier elimination in dense linear orders"
   15.10  
   15.11  
   15.12 @@ -546,7 +546,7 @@
   15.13  use "~~/src/HOL/Tools/Qelim/ferrante_rackoff.ML"
   15.14  
   15.15  method_setup ferrack = {*
   15.16 -  Method.ctxt_args (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   15.17 +  Scan.succeed (SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
   15.18  *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
   15.19  
   15.20  subsection {* Ferrante and Rackoff algorithm over ordered fields *}
    16.1 --- a/src/HOL/Groebner_Basis.thy	Mon Mar 16 17:51:24 2009 +0100
    16.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Mar 16 18:24:30 2009 +0100
    16.3 @@ -253,7 +253,7 @@
    16.4  
    16.5  
    16.6  method_setup sring_norm = {*
    16.7 -  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
    16.8 +  Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
    16.9  *} "semiring normalizer"
   16.10  
   16.11  
   16.12 @@ -427,10 +427,9 @@
   16.13   val any_keyword = keyword addN || keyword delN
   16.14   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   16.15  in
   16.16 -fn src => Method.syntax 
   16.17 -    ((Scan.optional (keyword addN |-- thms) []) -- 
   16.18 -    (Scan.optional (keyword delN |-- thms) [])) src 
   16.19 - #> (fn ((add_ths, del_ths), ctxt) => 
   16.20 +  ((Scan.optional (keyword addN |-- thms) []) -- 
   16.21 +   (Scan.optional (keyword delN |-- thms) [])) >>
   16.22 +  (fn (add_ths, del_ths) => fn ctxt =>
   16.23         SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
   16.24  end
   16.25  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
    17.1 --- a/src/HOL/Hoare/Hoare.thy	Mon Mar 16 17:51:24 2009 +0100
    17.2 +++ b/src/HOL/Hoare/Hoare.thy	Mon Mar 16 18:24:30 2009 +0100
    17.3 @@ -234,11 +234,11 @@
    17.4  use "hoare_tac.ML"
    17.5  
    17.6  method_setup vcg = {*
    17.7 -  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    17.8 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    17.9    "verification condition generator"
   17.10  
   17.11  method_setup vcg_simp = {*
   17.12 -  Method.ctxt_args (fn ctxt =>
   17.13 +  Scan.succeed (fn ctxt =>
   17.14      SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   17.15    "verification condition generator plus simplification"
   17.16  
    18.1 --- a/src/HOL/Hoare/HoareAbort.thy	Mon Mar 16 17:51:24 2009 +0100
    18.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Mon Mar 16 18:24:30 2009 +0100
    18.3 @@ -246,11 +246,11 @@
    18.4  use "hoare_tac.ML"
    18.5  
    18.6  method_setup vcg = {*
    18.7 -  Method.ctxt_args (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    18.8 +  Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *}
    18.9    "verification condition generator"
   18.10  
   18.11  method_setup vcg_simp = {*
   18.12 -  Method.ctxt_args (fn ctxt =>
   18.13 +  Scan.succeed (fn ctxt =>
   18.14      SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
   18.15    "verification condition generator plus simplification"
   18.16  
    19.1 --- a/src/HOL/HoareParallel/OG_Tactics.thy	Mon Mar 16 17:51:24 2009 +0100
    19.2 +++ b/src/HOL/HoareParallel/OG_Tactics.thy	Mon Mar 16 18:24:30 2009 +0100
    19.3 @@ -465,21 +465,21 @@
    19.4  Isabelle proofs. *}
    19.5  
    19.6  method_setup oghoare = {*
    19.7 -  Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
    19.8 +  Scan.succeed (K (SIMPLE_METHOD' oghoare_tac)) *}
    19.9    "verification condition generator for the oghoare logic"
   19.10  
   19.11  method_setup annhoare = {*
   19.12 -  Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
   19.13 +  Scan.succeed (K (SIMPLE_METHOD' annhoare_tac)) *}
   19.14    "verification condition generator for the ann_hoare logic"
   19.15  
   19.16  method_setup interfree_aux = {*
   19.17 -  Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
   19.18 +  Scan.succeed (K (SIMPLE_METHOD' interfree_aux_tac)) *}
   19.19    "verification condition generator for interference freedom tests"
   19.20  
   19.21  text {* Tactics useful for dealing with the generated verification conditions: *}
   19.22  
   19.23  method_setup conjI_tac = {*
   19.24 -  Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
   19.25 +  Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac)))) *}
   19.26    "verification condition generator for interference freedom tests"
   19.27  
   19.28  ML {*
   19.29 @@ -490,7 +490,7 @@
   19.30  *}
   19.31  
   19.32  method_setup disjE_tac = {*
   19.33 -  Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
   19.34 +  Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac)))) *}
   19.35    "verification condition generator for interference freedom tests"
   19.36  
   19.37  end
    20.1 --- a/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 17:51:24 2009 +0100
    20.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Mon Mar 16 18:24:30 2009 +0100
    20.3 @@ -454,7 +454,7 @@
    20.4  use "~~/src/HOL/Hoare/hoare_tac.ML"
    20.5  
    20.6  method_setup hoare = {*
    20.7 -  Method.ctxt_args (fn ctxt =>
    20.8 +  Scan.succeed (fn ctxt =>
    20.9      (SIMPLE_METHOD'
   20.10         (hoare_tac ctxt (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_comp"}] ))))) *}
   20.11    "verification condition generator for Hoare logic"
    21.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 16 17:51:24 2009 +0100
    21.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 16 18:24:30 2009 +0100
    21.3 @@ -134,8 +134,8 @@
    21.4     (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
    21.5     THEN' asm_full_simp_tac (ss2 addsimps ths)
    21.6   in
    21.7 -  Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
    21.8 -end
    21.9 +  Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
   21.10 + end
   21.11  *} "Lifts trivial vector statements to real arith statements"
   21.12  
   21.13  lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
   21.14 @@ -948,7 +948,7 @@
   21.15  
   21.16  use "normarith.ML"
   21.17  
   21.18 -method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   21.19 +method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
   21.20  *} "Proves simple linear statements about vector norms"
   21.21  
   21.22  
    22.1 --- a/src/HOL/Library/Eval_Witness.thy	Mon Mar 16 17:51:24 2009 +0100
    22.2 +++ b/src/HOL/Library/Eval_Witness.thy	Mon Mar 16 18:24:30 2009 +0100
    22.3 @@ -1,7 +1,5 @@
    22.4  (*  Title:      HOL/Library/Eval_Witness.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Alexander Krauss, TU Muenchen
    22.7 -
    22.8  *)
    22.9  
   22.10  header {* Evaluation Oracle with ML witnesses *}
   22.11 @@ -78,15 +76,10 @@
   22.12  
   22.13  
   22.14  method_setup eval_witness = {*
   22.15 -let
   22.16 -
   22.17 -fun eval_tac ws = CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i)
   22.18 -
   22.19 -in
   22.20 -  Method.simple_args (Scan.repeat Args.name) (fn ws => fn _ =>
   22.21 -    SIMPLE_METHOD' (eval_tac ws))
   22.22 -end
   22.23 -*} "Evaluation with ML witnesses"
   22.24 +  Scan.lift (Scan.repeat Args.name) >>
   22.25 +  (fn ws => K (SIMPLE_METHOD'
   22.26 +    (CSUBGOAL (fn (ct, i) => rtac (eval_witness_oracle (ct, ws)) i))))
   22.27 +*} "evaluation with ML witnesses"
   22.28  
   22.29  
   22.30  subsection {* Toy Examples *}
    23.1 --- a/src/HOL/Library/Reflection.thy	Mon Mar 16 17:51:24 2009 +0100
    23.2 +++ b/src/HOL/Library/Reflection.thy	Mon Mar 16 18:24:30 2009 +0100
    23.3 @@ -16,10 +16,10 @@
    23.4  
    23.5  use "reflection.ML"
    23.6  
    23.7 -method_setup reify = {* fn src =>
    23.8 -  Method.syntax (Attrib.thms --
    23.9 -    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
   23.10 -  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
   23.11 +method_setup reify = {*
   23.12 +  Attrib.thms --
   23.13 +    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
   23.14 +  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
   23.15  *} "partial automatic reification"
   23.16  
   23.17  method_setup reflection = {* 
   23.18 @@ -30,16 +30,17 @@
   23.19    val any_keyword = keyword onlyN || keyword rulesN;
   23.20    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
   23.21    val terms = thms >> map (term_of o Drule.dest_term);
   23.22 -  fun optional scan = Scan.optional scan [];
   23.23 -in fn src =>
   23.24 -  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
   23.25 -    (fn (((eqs,ths),to), ctxt) => 
   23.26 -      let 
   23.27 -        val (ceqs,cths) = Reify_Data.get ctxt 
   23.28 -        val corr_thms = ths@cths
   23.29 -        val raw_eqs = eqs@ceqs
   23.30 -      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
   23.31 -     end) end
   23.32 -*} "reflection method"
   23.33 +in
   23.34 +  thms --
   23.35 +  Scan.optional (keyword rulesN |-- thms) [] --
   23.36 +  Scan.option (keyword onlyN |-- Args.term) >>
   23.37 +  (fn ((eqs,ths),to) => fn ctxt =>
   23.38 +    let 
   23.39 +      val (ceqs,cths) = Reify_Data.get ctxt 
   23.40 +      val corr_thms = ths@cths
   23.41 +      val raw_eqs = eqs@ceqs
   23.42 +    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
   23.43 +end
   23.44 +*} "reflection"
   23.45  
   23.46  end
    24.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Mar 16 17:51:24 2009 +0100
    24.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Mon Mar 16 18:24:30 2009 +0100
    24.3 @@ -978,9 +978,8 @@
    24.4    val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym]
    24.5    val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}]
    24.6    fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2
    24.7 -  in Method.thms_args (SIMPLE_METHOD' o tac) end
    24.8 -
    24.9 -*} "Reduces goals about net"
   24.10 +  in Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (tac ths))) end
   24.11 +*} "reduces goals about net"
   24.12  
   24.13  lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a"
   24.14    apply (net at_def)
    25.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 16 17:51:24 2009 +0100
    25.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 16 18:24:30 2009 +0100
    25.3 @@ -199,9 +199,10 @@
    25.4      (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
    25.5       (Scan.succeed false);
    25.6  
    25.7 -val setup_generate_fresh =
    25.8 -  Method.goal_args_ctxt' Args.tyname (fn ctxt => generate_fresh_tac) 
    25.9 +fun setup_generate_fresh x =
   25.10 +  (Args.goal_spec -- Args.tyname >>
   25.11 +    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
   25.12  
   25.13 -val setup_fresh_fun_simp =
   25.14 -  Method.simple_args options_syntax 
   25.15 -  (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
   25.16 +fun setup_fresh_fun_simp x =
   25.17 +  (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
   25.18 +
    26.1 --- a/src/HOL/Nominal/nominal_induct.ML	Mon Mar 16 17:51:24 2009 +0100
    26.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Mon Mar 16 18:24:30 2009 +0100
    26.3 @@ -8,7 +8,7 @@
    26.4    val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
    26.5      (string * typ) list -> (string * typ) list list -> thm list ->
    26.6      thm list -> int -> RuleCases.cases_tactic
    26.7 -  val nominal_induct_method: Method.src -> Proof.context -> Proof.method
    26.8 +  val nominal_induct_method: (Proof.context -> Proof.method) context_parser
    26.9  end =
   26.10  struct
   26.11  
   26.12 @@ -152,11 +152,10 @@
   26.13  
   26.14  in
   26.15  
   26.16 -fun nominal_induct_method src =
   26.17 -  Method.syntax
   26.18 -   (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   26.19 -    avoiding -- fixing -- rule_spec) src
   26.20 -  #> (fn ((((x, y), z), w), ctxt) =>
   26.21 +val nominal_induct_method =
   26.22 +  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
   26.23 +  avoiding -- fixing -- rule_spec >>
   26.24 +  (fn (((x, y), z), w) => fn ctxt =>
   26.25      RAW_METHOD_CASES (fn facts =>
   26.26        HEADGOAL (nominal_induct_tac ctxt x y z w facts)));
   26.27  
    27.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Mon Mar 16 17:51:24 2009 +0100
    27.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Mon Mar 16 18:24:30 2009 +0100
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      HOL/Nominal/nominal_permeq.ML
    27.5 -    ID:         $Id$
    27.6      Authors:    Christian Urban, Julien Narboux, TU Muenchen
    27.7  
    27.8  Methods for simplifying permutations and
    27.9 @@ -36,16 +35,16 @@
   27.10    val finite_guess_tac : simpset -> int -> tactic
   27.11    val fresh_guess_tac : simpset -> int -> tactic
   27.12  
   27.13 -  val perm_simp_meth : Method.src -> Proof.context -> Proof.method
   27.14 -  val perm_simp_meth_debug : Method.src -> Proof.context -> Proof.method
   27.15 -  val perm_extend_simp_meth : Method.src -> Proof.context -> Proof.method
   27.16 -  val perm_extend_simp_meth_debug : Method.src -> Proof.context -> Proof.method
   27.17 -  val supports_meth : Method.src -> Proof.context -> Proof.method
   27.18 -  val supports_meth_debug : Method.src -> Proof.context -> Proof.method
   27.19 -  val finite_guess_meth : Method.src -> Proof.context -> Proof.method
   27.20 -  val finite_guess_meth_debug : Method.src -> Proof.context -> Proof.method
   27.21 -  val fresh_guess_meth : Method.src -> Proof.context -> Proof.method
   27.22 -  val fresh_guess_meth_debug : Method.src -> Proof.context -> Proof.method
   27.23 +  val perm_simp_meth : (Proof.context -> Proof.method) context_parser
   27.24 +  val perm_simp_meth_debug : (Proof.context -> Proof.method) context_parser
   27.25 +  val perm_extend_simp_meth : (Proof.context -> Proof.method) context_parser
   27.26 +  val perm_extend_simp_meth_debug : (Proof.context -> Proof.method) context_parser
   27.27 +  val supports_meth : (Proof.context -> Proof.method) context_parser
   27.28 +  val supports_meth_debug : (Proof.context -> Proof.method) context_parser
   27.29 +  val finite_guess_meth : (Proof.context -> Proof.method) context_parser
   27.30 +  val finite_guess_meth_debug : (Proof.context -> Proof.method) context_parser
   27.31 +  val fresh_guess_meth : (Proof.context -> Proof.method) context_parser
   27.32 +  val fresh_guess_meth_debug : (Proof.context -> Proof.method) context_parser
   27.33  end
   27.34  
   27.35  structure NominalPermeq : NOMINAL_PERMEQ =
   27.36 @@ -400,26 +399,24 @@
   27.37    Args.parens (Args.$$$ asm_lrN) >> K (perm_asm_lr_simp_tac_i NO_DEBUG_tac) ||
   27.38    Scan.succeed (perm_asm_full_simp_tac_i NO_DEBUG_tac));
   27.39  
   27.40 -fun perm_simp_method (prems, tac) ctxt = METHOD (fn facts =>
   27.41 -   HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   27.42 -       ((CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
   27.43 -
   27.44 -val perm_simp_meth = Method.sectioned_args
   27.45 -     (Args.bang_facts -- Scan.lift perm_simp_options)
   27.46 -     (Simplifier.simp_modifiers') perm_simp_method
   27.47 +val perm_simp_meth =
   27.48 +  Args.bang_facts -- Scan.lift perm_simp_options --|
   27.49 +  Method.sections (Simplifier.simp_modifiers') >>
   27.50 +  (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
   27.51 +    HEADGOAL (Method.insert_tac (prems @ facts) THEN'
   27.52 +      (CHANGED_PROP oo tac) (local_simpset_of ctxt))));
   27.53  
   27.54  (* setup so that the simpset is used which is active at the moment when the tactic is called *)
   27.55  fun local_simp_meth_setup tac =
   27.56 -  Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   27.57 -  (SIMPLE_METHOD' o tac o local_simpset_of) ;
   27.58 +  Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
   27.59 +  (K (SIMPLE_METHOD' o tac o local_simpset_of));
   27.60  
   27.61  (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
   27.62  
   27.63  fun basic_simp_meth_setup debug tac =
   27.64 -  Method.sectioned_args 
   27.65 -   (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
   27.66 -   (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   27.67 -   (fn _ => SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
   27.68 +  Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
   27.69 +  Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
   27.70 +  (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o local_simpset_of));
   27.71  
   27.72  val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
   27.73  val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
    28.1 --- a/src/HOL/Presburger.thy	Mon Mar 16 17:51:24 2009 +0100
    28.2 +++ b/src/HOL/Presburger.thy	Mon Mar 16 18:24:30 2009 +0100
    28.3 @@ -455,12 +455,11 @@
    28.4   val any_keyword = keyword addN || keyword delN || simple_keyword elimN
    28.5   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    28.6  in
    28.7 -  fn src => Method.syntax 
    28.8 -   ((Scan.optional (simple_keyword elimN >> K false) true) -- 
    28.9 -    (Scan.optional (keyword addN |-- thms) []) -- 
   28.10 -    (Scan.optional (keyword delN |-- thms) [])) src 
   28.11 -  #> (fn (((elim, add_ths), del_ths),ctxt) => 
   28.12 -         SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
   28.13 +  Scan.optional (simple_keyword elimN >> K false) true --
   28.14 +  Scan.optional (keyword addN |-- thms) [] --
   28.15 +  Scan.optional (keyword delN |-- thms) [] >>
   28.16 +  (fn ((elim, add_ths), del_ths) => fn ctxt =>
   28.17 +    SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt))
   28.18  end
   28.19  *} "Cooper's algorithm for Presburger arithmetic"
   28.20  
    29.1 --- a/src/HOL/Prolog/HOHH.thy	Mon Mar 16 17:51:24 2009 +0100
    29.2 +++ b/src/HOL/Prolog/HOHH.thy	Mon Mar 16 18:24:30 2009 +0100
    29.3 @@ -11,11 +11,11 @@
    29.4  begin
    29.5  
    29.6  method_setup ptac =
    29.7 -  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
    29.8 +  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
    29.9    "Basic Lambda Prolog interpreter"
   29.10  
   29.11  method_setup prolog =
   29.12 -  {* Method.thms_ctxt_args (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   29.13 +  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
   29.14    "Lambda Prolog interpreter"
   29.15  
   29.16  consts
    30.1 --- a/src/HOL/SAT.thy	Mon Mar 16 17:51:24 2009 +0100
    30.2 +++ b/src/HOL/SAT.thy	Mon Mar 16 18:24:30 2009 +0100
    30.3 @@ -1,5 +1,4 @@
    30.4  (*  Title:      HOL/SAT.thy
    30.5 -    ID:         $Id$
    30.6      Author:     Alwen Tiu, Tjark Weber
    30.7      Copyright   2005
    30.8  
    30.9 @@ -28,10 +27,10 @@
   30.10  
   30.11  ML {* structure sat = SATFunc(structure cnf = cnf); *}
   30.12  
   30.13 -method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
   30.14 +method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
   30.15    "SAT solver"
   30.16  
   30.17 -method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
   30.18 +method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
   30.19    "SAT solver (with definitional CNF)"
   30.20  
   30.21  end
    31.1 --- a/src/HOL/SET-Protocol/Cardholder_Registration.thy	Mon Mar 16 17:51:24 2009 +0100
    31.2 +++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy	Mon Mar 16 18:24:30 2009 +0100
    31.3 @@ -541,10 +541,11 @@
    31.4  by (blast intro: analz_mono [THEN [2] rev_subsetD])
    31.5  
    31.6  method_setup valid_certificate_tac = {*
    31.7 -  Method.goal_args (Scan.succeed ()) (fn () => fn i =>
    31.8 -    EVERY [ftac @{thm Gets_certificate_valid} i,
    31.9 -           assume_tac i,
   31.10 -           etac conjE i, REPEAT (hyp_subst_tac i)])
   31.11 +  Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
   31.12 +    (fn i =>
   31.13 +      EVERY [ftac @{thm Gets_certificate_valid} i,
   31.14 +             assume_tac i,
   31.15 +             etac conjE i, REPEAT (hyp_subst_tac i)])))
   31.16  *} ""
   31.17  
   31.18  text{*The @{text "(no_asm)"} attribute is essential, since it retains
    32.1 --- a/src/HOL/SET-Protocol/EventSET.thy	Mon Mar 16 17:51:24 2009 +0100
    32.2 +++ b/src/HOL/SET-Protocol/EventSET.thy	Mon Mar 16 18:24:30 2009 +0100
    32.3 @@ -189,7 +189,7 @@
    32.4  *}
    32.5  
    32.6  method_setup analz_mono_contra = {*
    32.7 -    Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *}
    32.8 +    Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *}
    32.9      "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P"
   32.10  
   32.11  end
    33.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Mon Mar 16 17:51:24 2009 +0100
    33.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Mon Mar 16 18:24:30 2009 +0100
    33.3 @@ -940,17 +940,17 @@
    33.4  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    33.5  
    33.6  method_setup spy_analz = {*
    33.7 -    Method.ctxt_args (fn ctxt =>
    33.8 +    Scan.succeed (fn ctxt =>
    33.9          SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
   33.10      "for proving the Fake case when analz is involved"
   33.11  
   33.12  method_setup atomic_spy_analz = {*
   33.13 -    Method.ctxt_args (fn ctxt =>
   33.14 +    Scan.succeed (fn ctxt =>
   33.15          SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
   33.16      "for debugging spy_analz"
   33.17  
   33.18  method_setup Fake_insert_simp = {*
   33.19 -    Method.ctxt_args (fn ctxt =>
   33.20 +    Scan.succeed (fn ctxt =>
   33.21          SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
   33.22      "for debugging spy_analz"
   33.23  
    34.1 --- a/src/HOL/SET-Protocol/PublicSET.thy	Mon Mar 16 17:51:24 2009 +0100
    34.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Mon Mar 16 18:24:30 2009 +0100
    34.3 @@ -371,7 +371,7 @@
    34.4  *}
    34.5  
    34.6  method_setup possibility = {*
    34.7 -    Method.ctxt_args (fn ctxt =>
    34.8 +    Scan.succeed (fn ctxt =>
    34.9          SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
   34.10      "for proving possibility theorems"
   34.11  
    35.1 --- a/src/HOL/SET-Protocol/Purchase.thy	Mon Mar 16 17:51:24 2009 +0100
    35.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Mon Mar 16 18:24:30 2009 +0100
    35.3 @@ -477,9 +477,10 @@
    35.4  by (frule Gets_imp_Says, auto)
    35.5  
    35.6  method_setup valid_certificate_tac = {*
    35.7 -  Method.goal_args (Scan.succeed ()) (fn () => fn i =>
    35.8 -    EVERY [ftac @{thm Gets_certificate_valid} i,
    35.9 -           assume_tac i, REPEAT (hyp_subst_tac i)])
   35.10 +  Args.goal_spec >> (fn quant =>
   35.11 +    K (SIMPLE_METHOD'' quant (fn i =>
   35.12 +      EVERY [ftac @{thm Gets_certificate_valid} i,
   35.13 +             assume_tac i, REPEAT (hyp_subst_tac i)])))
   35.14  *} ""
   35.15  
   35.16  
    36.1 --- a/src/HOL/Transitive_Closure.thy	Mon Mar 16 17:51:24 2009 +0100
    36.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Mar 16 18:24:30 2009 +0100
    36.3 @@ -695,16 +695,16 @@
    36.4  (* Optional methods *)
    36.5  
    36.6  method_setup trancl =
    36.7 -  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
    36.8 +  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}
    36.9    {* simple transitivity reasoner *}
   36.10  method_setup rtrancl =
   36.11 -  {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   36.12 +  {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}
   36.13    {* simple transitivity reasoner *}
   36.14  method_setup tranclp =
   36.15 -  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   36.16 +  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}
   36.17    {* simple transitivity reasoner (predicate version) *}
   36.18  method_setup rtranclp =
   36.19 -  {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   36.20 +  {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}
   36.21    {* simple transitivity reasoner (predicate version) *}
   36.22  
   36.23  end
    37.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Mar 16 17:51:24 2009 +0100
    37.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Mar 16 18:24:30 2009 +0100
    37.3 @@ -321,7 +321,7 @@
    37.4  *}
    37.5  
    37.6  method_setup record_auto = {*
    37.7 -  Method.ctxt_args (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
    37.8 +  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
    37.9  *} ""
   37.10  
   37.11  lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   37.12 @@ -713,7 +713,7 @@
   37.13  *}
   37.14  
   37.15  method_setup rename_client_map = {*
   37.16 -  Method.ctxt_args (fn ctxt =>
   37.17 +  Scan.succeed (fn ctxt =>
   37.18      SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
   37.19  *} ""
   37.20  
    38.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Mar 16 17:51:24 2009 +0100
    38.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Mar 16 18:24:30 2009 +0100
    38.3 @@ -124,7 +124,7 @@
    38.4  *}
    38.5  
    38.6  method_setup ns_induct = {*
    38.7 -    Method.ctxt_args (fn ctxt =>
    38.8 +    Scan.succeed (fn ctxt =>
    38.9          SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
   38.10      "for inductive reasoning about the Needham-Schroeder protocol"
   38.11  
    39.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 16 17:51:24 2009 +0100
    39.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Mon Mar 16 18:24:30 2009 +0100
    39.3 @@ -10,15 +10,13 @@
    39.4  uses "UNITY_tactics.ML" begin
    39.5  
    39.6  method_setup safety = {*
    39.7 -    Method.ctxt_args (fn ctxt =>
    39.8 +    Scan.succeed (fn ctxt =>
    39.9          SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
   39.10      "for proving safety properties"
   39.11  
   39.12  method_setup ensures_tac = {*
   39.13 -    fn args => fn ctxt =>
   39.14 -        Method.goal_args' (Scan.lift Args.name_source)
   39.15 -           (ensures_tac (local_clasimpset_of ctxt))
   39.16 -           args ctxt *}
   39.17 -    "for proving progress properties"
   39.18 +  Args.goal_spec -- Scan.lift Args.name_source >>
   39.19 +  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
   39.20 +*} "for proving progress properties"
   39.21  
   39.22  end
    40.1 --- a/src/HOL/Word/WordArith.thy	Mon Mar 16 17:51:24 2009 +0100
    40.2 +++ b/src/HOL/Word/WordArith.thy	Mon Mar 16 18:24:30 2009 +0100
    40.3 @@ -530,7 +530,7 @@
    40.4  *}
    40.5  
    40.6  method_setup uint_arith = 
    40.7 -  "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)" 
    40.8 +  {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
    40.9    "solving word arithmetic via integers and arith"
   40.10  
   40.11  
   40.12 @@ -1086,7 +1086,7 @@
   40.13  *}
   40.14  
   40.15  method_setup unat_arith = 
   40.16 -  "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)" 
   40.17 +  {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
   40.18    "solving word arithmetic via natural numbers and arith"
   40.19  
   40.20  lemma no_plus_overflow_unat_size: 
    41.1 --- a/src/HOL/ex/Binary.thy	Mon Mar 16 17:51:24 2009 +0100
    41.2 +++ b/src/HOL/ex/Binary.thy	Mon Mar 16 18:24:30 2009 +0100
    41.3 @@ -174,7 +174,7 @@
    41.4  simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
    41.5  
    41.6  method_setup binary_simp = {*
    41.7 -  Method.no_args (SIMPLE_METHOD'
    41.8 +  Scan.succeed (K (SIMPLE_METHOD'
    41.9      (full_simp_tac
   41.10        (HOL_basic_ss
   41.11          addsimps @{thms binary_simps}
   41.12 @@ -183,7 +183,7 @@
   41.13            @{simproc binary_nat_less},
   41.14            @{simproc binary_nat_diff},
   41.15            @{simproc binary_nat_div},
   41.16 -          @{simproc binary_nat_mod}])))
   41.17 +          @{simproc binary_nat_mod}]))))
   41.18  *} "binary simplification"
   41.19  
   41.20  
    42.1 --- a/src/HOL/ex/SAT_Examples.thy	Mon Mar 16 17:51:24 2009 +0100
    42.2 +++ b/src/HOL/ex/SAT_Examples.thy	Mon Mar 16 18:24:30 2009 +0100
    42.3 @@ -83,7 +83,7 @@
    42.4  ML {* reset quick_and_dirty; *}
    42.5  
    42.6  method_setup rawsat =
    42.7 -  {* Method.no_args (SIMPLE_METHOD' sat.rawsat_tac) *}
    42.8 +  {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *}
    42.9    "SAT solver (no preprocessing)"
   42.10  
   42.11  (* ML {* Toplevel.profiling := 1; *} *)
    43.1 --- a/src/Sequents/ILL.thy	Mon Mar 16 17:51:24 2009 +0100
    43.2 +++ b/src/Sequents/ILL.thy	Mon Mar 16 18:24:30 2009 +0100
    43.3 @@ -146,7 +146,7 @@
    43.4  *}
    43.5  
    43.6  method_setup best_lazy =
    43.7 -  {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
    43.8 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
    43.9    "lazy classical reasoning"
   43.10  
   43.11  lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
   43.12 @@ -282,10 +282,10 @@
   43.13  
   43.14  
   43.15  method_setup best_safe =
   43.16 -  {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
   43.17 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
   43.18  
   43.19  method_setup best_power =
   43.20 -  {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
   43.21 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
   43.22  
   43.23  
   43.24  (* Some examples from Troelstra and van Dalen *)
    44.1 --- a/src/Sequents/LK0.thy	Mon Mar 16 17:51:24 2009 +0100
    44.2 +++ b/src/Sequents/LK0.thy	Mon Mar 16 18:24:30 2009 +0100
    44.3 @@ -240,23 +240,23 @@
    44.4  *}
    44.5  
    44.6  method_setup fast_prop =
    44.7 -  {* Method.no_args (SIMPLE_METHOD' (fast_tac prop_pack)) *}
    44.8 +  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
    44.9    "propositional reasoning"
   44.10  
   44.11  method_setup fast =
   44.12 -  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_pack)) *}
   44.13 +  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
   44.14    "classical reasoning"
   44.15  
   44.16  method_setup fast_dup =
   44.17 -  {* Method.no_args (SIMPLE_METHOD' (fast_tac LK_dup_pack)) *}
   44.18 +  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
   44.19    "classical reasoning"
   44.20  
   44.21  method_setup best =
   44.22 -  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_pack)) *}
   44.23 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
   44.24    "classical reasoning"
   44.25  
   44.26  method_setup best_dup =
   44.27 -  {* Method.no_args (SIMPLE_METHOD' (best_tac LK_dup_pack)) *}
   44.28 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
   44.29    "classical reasoning"
   44.30  
   44.31  
    45.1 --- a/src/Sequents/S4.thy	Mon Mar 16 17:51:24 2009 +0100
    45.2 +++ b/src/Sequents/S4.thy	Mon Mar 16 18:24:30 2009 +0100
    45.3 @@ -45,7 +45,7 @@
    45.4  *}
    45.5  
    45.6  method_setup S4_solve =
    45.7 -  {* Method.no_args (SIMPLE_METHOD (S4_Prover.solve_tac 2)) *} "S4 solver"
    45.8 +  {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver"
    45.9  
   45.10  
   45.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    46.1 --- a/src/Sequents/S43.thy	Mon Mar 16 17:51:24 2009 +0100
    46.2 +++ b/src/Sequents/S43.thy	Mon Mar 16 18:24:30 2009 +0100
    46.3 @@ -92,8 +92,8 @@
    46.4  
    46.5  
    46.6  method_setup S43_solve = {*
    46.7 -  Method.no_args (SIMPLE_METHOD
    46.8 -    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
    46.9 +  Scan.succeed (K (SIMPLE_METHOD
   46.10 +    (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
   46.11  *} "S4 solver"
   46.12  
   46.13  
    47.1 --- a/src/Sequents/T.thy	Mon Mar 16 17:51:24 2009 +0100
    47.2 +++ b/src/Sequents/T.thy	Mon Mar 16 18:24:30 2009 +0100
    47.3 @@ -44,7 +44,7 @@
    47.4  *}
    47.5  
    47.6  method_setup T_solve =
    47.7 -  {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver"
    47.8 +  {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver"
    47.9  
   47.10  
   47.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    48.1 --- a/src/ZF/UNITY/Constrains.thy	Mon Mar 16 17:51:24 2009 +0100
    48.2 +++ b/src/ZF/UNITY/Constrains.thy	Mon Mar 16 18:24:30 2009 +0100
    48.3 @@ -496,11 +496,11 @@
    48.4  setup ProgramDefs.setup
    48.5  
    48.6  method_setup safety = {*
    48.7 -  Method.ctxt_args (SIMPLE_METHOD' o constrains_tac) *}
    48.8 +  Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
    48.9    "for proving safety properties"
   48.10  
   48.11  method_setup always = {*
   48.12 -  Method.ctxt_args (SIMPLE_METHOD' o always_tac) *}
   48.13 +  Scan.succeed (SIMPLE_METHOD' o always_tac) *}
   48.14    "for proving invariants"
   48.15  
   48.16  end
    49.1 --- a/src/ZF/UNITY/SubstAx.thy	Mon Mar 16 17:51:24 2009 +0100
    49.2 +++ b/src/ZF/UNITY/SubstAx.thy	Mon Mar 16 18:24:30 2009 +0100
    49.3 @@ -377,9 +377,8 @@
    49.4  *}
    49.5  
    49.6  method_setup ensures_tac = {*
    49.7 -    fn args => fn ctxt =>
    49.8 -        Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt)
    49.9 -           args ctxt *}
   49.10 -    "for proving progress properties"
   49.11 +    Args.goal_spec -- Scan.lift Args.name_source >>
   49.12 +    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
   49.13 +*} "for proving progress properties"
   49.14  
   49.15  end