--- 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>