--- a/doc-src/TutorialI/Protocol/Message.thy Fri Mar 13 19:10:46 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Fri Mar 13 19:53:09 2009 +0100
@@ -919,18 +919,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o gen_spy_analz_tac o local_clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
+ Method.ctxt_args (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
"for debugging spy_analz"
--- a/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:10:46 2009 +0100
+++ b/doc-src/TutorialI/Protocol/Public.thy Fri Mar 13 19:53:09 2009 +0100
@@ -161,8 +161,7 @@
resolve_tac [refl, conjI, @{thm Nonce_supply}]));
*}
-method_setup possibility = {*
- Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
+method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *}
"for proving possibility theorems"
end
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 13 19:10:46 2009 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri Mar 13 19:53:09 2009 +0100
@@ -121,11 +121,10 @@
Method.simple_args
(Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
curry (Library.foldl op |>) true)
- (fn q => fn ctxt => meth ctxt q 1)
+ (fn q => fn ctxt => meth ctxt q)
end;
-fun linz_method ctxt q i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN linz_tac ctxt q i);
+fun linz_method ctxt q = SIMPLE_METHOD' (linz_tac ctxt q);
val setup =
Method.add_method ("cooper",
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 13 19:10:46 2009 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Mar 13 19:53:09 2009 +0100
@@ -150,11 +150,10 @@
Method.simple_args
(Scan.optional (Args.$$$ "(" |-- Scan.repeat1 parse_flag --| Args.$$$ ")") [] >>
curry (Library.foldl op |>) true)
- (fn q => fn ctxt => meth ctxt q 1)
+ (fn q => fn ctxt => meth ctxt q)
end;
-fun mir_method ctxt q i = Method.METHOD (fn facts =>
- Method.insert_tac facts 1 THEN mir_tac ctxt q i);
+fun mir_method ctxt q = SIMPLE_METHOD' (mir_tac ctxt q);
val setup =
Method.add_method ("mir",
--- a/src/HOL/Word/WordArith.thy Fri Mar 13 19:10:46 2009 +0100
+++ b/src/HOL/Word/WordArith.thy Fri Mar 13 19:53:09 2009 +0100
@@ -530,7 +530,7 @@
*}
method_setup uint_arith =
- "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (uint_arith_tac ctxt 1))"
+ "Method.ctxt_args (SIMPLE_METHOD' o uint_arith_tac)"
"solving word arithmetic via integers and arith"
@@ -1086,7 +1086,7 @@
*}
method_setup unat_arith =
- "Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (unat_arith_tac ctxt 1))"
+ "Method.ctxt_args (SIMPLE_METHOD' o unat_arith_tac)"
"solving word arithmetic via natural numbers and arith"
lemma no_plus_overflow_unat_size: