Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Method.SIMPLE_METHOD';
authorwenzelm
Mon, 28 Aug 2000 20:31:00 +0200
changeset 9705 8eecca293907
parent 9704 c2f2f70bbb60
child 9706 8e48a19fc81e
Method.SIMPLE_METHOD';
src/HOL/Tools/record_package.ML file | annotate | diff | comparison | revisions
src/Provers/hypsubst.ML file | annotate | diff | comparison | revisions 
--- 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");
 
 
--- 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 *)
isabelle