src/Provers/hypsubst.ML
changeset 18708 4b3dadb4fe33
parent 17896 66902148c436
child 20074 b4d0b545df01
     1.1 --- a/src/Provers/hypsubst.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -58,7 +58,7 @@
     1.4    val inspect_pair           : bool -> bool -> term * term * typ -> bool
     1.5    val mk_eqs                 : bool -> thm -> thm list
     1.6    val stac		     : thm -> int -> tactic
     1.7 -  val hypsubst_setup         : (theory -> theory) list
     1.8 +  val hypsubst_setup         : theory -> theory
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -242,8 +242,8 @@
    1.13  (* theory setup *)
    1.14  
    1.15  val hypsubst_setup =
    1.16 - [Method.add_methods
    1.17 -  [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
    1.18 -   ("simplesubst", subst_meth, "simple substitution")]];
    1.19 +  Method.add_methods
    1.20 +    [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
    1.21 +     ("simplesubst", subst_meth, "simple substitution")];
    1.22  
    1.23  end;