# HG changeset patch
# User wenzelm
# Date 966257627 -7200
# Node ID abbd48606a0a981eb410ce846591863861ef8f6b
# Parent  590d36e059d164f5669c073fa4aae2f2123c1242
added hypsubst;

diff -r 590d36e059d1 -r abbd48606a0a src/Provers/hypsubst.ML
--- 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;