src/Provers/hypsubst.ML
changeset 9705 8eecca293907
parent 9628 53a62fd8b2dc
child 9893 93d2fde0306c
--- a/src/Provers/hypsubst.ML	Mon Aug 28 20:30:47 2000 +0200
+++ b/src/Provers/hypsubst.ML	Mon Aug 28 20:31:00 2000 +0200
@@ -256,8 +256,8 @@
 
 (* proof methods *)
 
-val subst_meth = Method.goal_args' Attrib.local_thm stac;
-val hyp_subst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac);
+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);
 
 
 (* attributes *)