# HG changeset patch
# User wenzelm
# Date 1243248545 -7200
# Node ID ed40b987a4748cbb1f6f552bc08f3a1a59d88ec0
# Parent  b3c7044d47b6ffd13d7348ec8dd0b65402e3d838
modernized method setup;

diff -r b3c7044d47b6 -r ed40b987a474 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Mon May 25 12:48:18 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML	Mon May 25 12:49:05 2009 +0200
@@ -100,13 +100,10 @@
     THEN (simp_tac cring_ss i)
   end);
 
-val comm_ring_meth =
-  Method.ctxt_args (SIMPLE_METHOD' o comm_ring_tac);
-
 val setup =
-  Method.add_method ("comm_ring", comm_ring_meth,
-    "reflective decision procedure for equalities over commutative rings") #>
-  Method.add_method ("algebra", comm_ring_meth,
-    "method for proving algebraic properties (same as comm_ring)");
+  Method.setup @{binding comm_ring} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
+    "reflective decision procedure for equalities over commutative rings" #>
+  Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o comm_ring_tac))
+    "method for proving algebraic properties (same as comm_ring)";
 
 end;
diff -r b3c7044d47b6 -r ed40b987a474 src/HOL/Tools/function_package/scnp_reconstruct.ML
--- a/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon May 25 12:48:18 2009 +0200
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Mon May 25 12:49:05 2009 +0200
@@ -416,14 +416,14 @@
 (* Method setup *)
 
 val orders =
-  (Scan.repeat1
+  Scan.repeat1
     ((Args.$$$ "max" >> K MAX) ||
      (Args.$$$ "min" >> K MIN) ||
      (Args.$$$ "ms" >> K MS))
-  || Scan.succeed [MAX, MS, MIN])
+  || Scan.succeed [MAX, MS, MIN]
 
-val setup = Method.add_method
-  ("sizechange", Method.sectioned_args (Scan.lift orders) clasimp_modifiers decomp_scnp,
-   "termination prover with graph decomposition and the NP subset of size change termination")
+val setup = Method.setup @{binding sizechange}
+  (Scan.lift orders --| Method.sections clasimp_modifiers >> decomp_scnp)
+  "termination prover with graph decomposition and the NP subset of size change termination"
 
 end