src/Provers/hypsubst.ML
changeset 9592 abbd48606a0a
parent 9532 36b9bc6eb454
child 9628 53a62fd8b2dc
--- 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;