src/Provers/eqsubst.ML

--- a/src/Provers/eqsubst.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/eqsubst.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -7,7 +7,7 @@
 
 signature EQSUBST =
 sig
-  val setup : (Theory.theory -> Theory.theory) list
+  val setup : theory -> theory
 end;
 
 structure EqSubst: EQSUBST =
@@ -337,6 +337,6 @@
 
 
 val setup =
-  [Method.add_method ("subst", subst_meth, "substiution with an equation")];
+  Method.add_method ("subst", subst_meth, "substiution with an equation");
 
 end;