--- a/src/Provers/hypsubst.ML Mon Aug 14 14:53:26 2000 +0200
+++ b/src/Provers/hypsubst.ML Mon Aug 14 14:53:47 2000 +0200
@@ -255,11 +255,11 @@
(* proof method setup *)
val subst_meth = Method.goal_args' Attrib.local_thm stac;
-val hypsubst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
+val hyp_subst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
val hypsubst_setup =
[Method.add_methods
- [("hypsubst", hypsubst_meth, "substitution using an assumption (improper)"),
+ [("hyp_subst", hyp_subst_meth, "substitution using an assumption (improper)"),
("subst", subst_meth, "substitution")]];
end;