src/Provers/hypsubst.ML
changeset 30515 bca05b17b618
parent 30510 4120fc59dd85
child 32957 675c0c7e6a37
--- a/src/Provers/hypsubst.ML	Fri Mar 13 23:32:40 2009 +0100
+++ b/src/Provers/hypsubst.ML	Fri Mar 13 23:50:05 2009 +0100
@@ -284,9 +284,10 @@
 (* theory setup *)
 
 val hypsubst_setup =
-  Method.add_methods
-    [("hypsubst", Method.no_args (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
-        "substitution using an assumption (improper)"),
-     ("simplesubst", Method.thm_args (SIMPLE_METHOD' o stac), "simple substitution")];
+  Method.setup @{binding hypsubst}
+    (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
+    "substitution using an assumption (improper)" #>
+  Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
+    "simple substitution";
 
 end;