diff -r 0c5cd369a643 -r 50b60f501b05 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/Cube/Example.thy	Tue Feb 10 14:48:26 2015 +0100
@@ -18,9 +18,9 @@
     (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))\<close>
 
 method_setup strip_asms =
-  \<open>Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-    REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
-    DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))\<close>
+  \<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>
 
 
 subsection \<open>Simple types\<close>