--- 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;
--- 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