# HG changeset patch
# User wenzelm
# Date 967487460 -7200
# Node ID 8eecca293907511a043303f10f7fe80158ca6496
# Parent  c2f2f70bbb6018335feac7c2492a01533a0177da
Method.SIMPLE_METHOD';

diff -r c2f2f70bbb60 -r 8eecca293907 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Aug 28 20:30:47 2000 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Aug 28 20:31:00 2000 +0200
@@ -524,7 +524,7 @@
 (* method *)
 
 val record_split_method =
-  ("record_split", Method.no_args (Method.METHOD0 (HEADGOAL record_split_tac)),
+  ("record_split", Method.no_args (Method.SIMPLE_METHOD' HEADGOAL record_split_tac),
     "split record fields");
 
 
diff -r c2f2f70bbb60 -r 8eecca293907 src/Provers/hypsubst.ML
--- 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 *)