src/Provers/hypsubst.ML
changeset 30510 4120fc59dd85
parent 27734 dcec1c564f05
child 30515 bca05b17b618
--- a/src/Provers/hypsubst.ML	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Provers/hypsubst.ML	Fri Mar 13 19:58:26 2009 +0100
@@ -285,8 +285,8 @@
 
 val hypsubst_setup =
   Method.add_methods
-    [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
+    [("hypsubst", Method.no_args (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
         "substitution using an assumption (improper)"),
-     ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
+     ("simplesubst", Method.thm_args (SIMPLE_METHOD' o stac), "simple substitution")];
 
 end;