src/Provers/hypsubst.ML
changeset 10821 dcb75538f542
parent 9893 93d2fde0306c
child 12262 11ff5f47df6e
--- a/src/Provers/hypsubst.ML	Sun Jan 07 21:40:49 2001 +0100
+++ b/src/Provers/hypsubst.ML	Sun Jan 07 21:41:56 2001 +0100
@@ -257,7 +257,8 @@
 (* proof methods *)
 
 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
-val hyp_subst_meth = Method.no_args (Method.SIMPLE_METHOD' HEADGOAL hyp_subst_tac);
+val hyp_subst_meth =
+  Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
 
 
 (* attributes *)