src/Provers/eqsubst.ML

 A proof method to perform a substiution using an equation.
 *)
 
 signature EQSUBST =
 sig
-  val setup : (Theory.theory -> Theory.theory) list
+  val setup : theory -> theory
 end;
 
 structure EqSubst: EQSUBST =
 struct
 

   #> (fn (ctxt, ((asmflag, occL), inthms)) =>
     (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
 
 
 val setup =
-  [Method.add_method ("subst", subst_meth, "substiution with an equation")];
+  Method.add_method ("subst", subst_meth, "substiution with an equation");
 
 end;