# HG changeset patch
# User wenzelm
# Date 1236970389 -3600
# Node ID e19d5b459a61542f6d31b90ace5cd13c858a54cc
# Parent  958cc116d03b4dbdfbcb4ab2ea7b3832bcbf1898
more regular method setup via SIMPLE_METHOD;

diff -r 958cc116d03b -r e19d5b459a61 doc-src/TutorialI/Protocol/Message.thy
--- 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"
 
 
diff -r 958cc116d03b -r e19d5b459a61 doc-src/TutorialI/Protocol/Public.thy
--- 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
diff -r 958cc116d03b -r e19d5b459a61 src/HOL/Decision_Procs/cooper_tac.ML
--- 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",
diff -r 958cc116d03b -r e19d5b459a61 src/HOL/Decision_Procs/mir_tac.ML
--- 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",
diff -r 958cc116d03b -r e19d5b459a61 src/HOL/Word/WordArith.thy
--- 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: