src/HOL/Library/comm_ring.ML

 signature COMM_RING =
 sig
   val comm_ring_tac : int -> tactic
   val comm_ring_method: int -> Proof.method
   val algebra_method: int -> Proof.method
-  val setup : (theory -> theory) list
+  val setup : theory -> theory
 end
 
 structure CommRing: COMM_RING =
 struct
 

 fun comm_ring_method i = Method.METHOD (fn facts =>
   Method.insert_tac facts 1 THEN comm_ring_tac i);
 val algebra_method = comm_ring_method;
 
 val setup =
-  [Method.add_method ("comm_ring",
+  Method.add_method ("comm_ring",
      Method.no_args (comm_ring_method 1),
-     "reflective decision procedure for equalities over commutative rings"),
-   Method.add_method ("algebra",
+     "reflective decision procedure for equalities over commutative rings") #>
+  Method.add_method ("algebra",
      Method.no_args (algebra_method 1),
-     "Method for proving algebraic properties: for now only comm_ring")];
+     "Method for proving algebraic properties: for now only comm_ring");
 
 end;