src/Provers/hypsubst.ML

   val vars_gen_hyp_subst_tac : bool -> int -> tactic
   val eq_var                 : bool -> bool -> term -> int * bool
   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;
 
 
 
 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =

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