diff -r 50b60f501b05 -r 14095f771781 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Tue Feb 10 14:48:26 2015 +0100
+++ b/src/Cube/Example.thy	Tue Feb 10 16:46:21 2015 +0100
@@ -10,17 +10,17 @@
   J. Functional Programming.\<close>
 
 method_setup depth_solve =
-  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-    (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
+  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
+    (DEPTH_SOLVE (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
 
 method_setup depth_solve1 =
-  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-    (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
+  \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
+    (DEPTH_SOLVE_1 (HEADGOAL (assume_tac ctxt ORELSE' resolve_tac ctxt (facts @ thms))))))\<close>
 
 method_setup strip_asms =
   \<open>Attrib.thms >> (fn thms => fn ctxt => METHOD (fn facts =>
     REPEAT (resolve_tac ctxt [@{thm strip_b}, @{thm strip_s}] 1 THEN
-    DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))\<close>
+    DEPTH_SOLVE_1 (assume_tac ctxt 1 ORELSE resolve_tac ctxt (facts @ thms) 1))))\<close>
 
 
 subsection \<open>Simple types\<close>