--- a/src/Provers/hypsubst.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/hypsubst.ML Thu Jan 19 21:22:08 2006 +0100
@@ -58,7 +58,7 @@
val inspect_pair : bool -> bool -> term * term * typ -> bool
val mk_eqs : bool -> thm -> thm list
val stac : thm -> int -> tactic
- val hypsubst_setup : (theory -> theory) list
+ val hypsubst_setup : theory -> theory
end;
@@ -242,8 +242,8 @@
(* theory setup *)
val hypsubst_setup =
- [Method.add_methods
- [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
- ("simplesubst", subst_meth, "simple substitution")]];
+ Method.add_methods
+ [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
+ ("simplesubst", subst_meth, "simple substitution")];
end;