diff -r e19d5b459a61 -r 4120fc59dd85 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Fri Mar 13 19:53:09 2009 +0100
+++ b/src/Cube/Example.thy	Fri Mar 13 19:58:26 2009 +0100
@@ -15,18 +15,18 @@
 *}
 
 method_setup depth_solve = {*
-  Method.thms_args (fn thms => Method.METHOD (fn facts =>
+  Method.thms_args (fn thms => METHOD (fn facts =>
   (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
 *} ""
 
 method_setup depth_solve1 = {*
-  Method.thms_args (fn thms => Method.METHOD (fn facts =>
+  Method.thms_args (fn thms => METHOD (fn facts =>
   (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
 *} ""
 
 method_setup strip_asms =  {*
   let val strip_b = thm "strip_b" and strip_s = thm "strip_s" in
-    Method.thms_args (fn thms => Method.METHOD (fn facts =>
+    Method.thms_args (fn thms => METHOD (fn facts =>
       REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
   end
 *} ""