--- a/src/Cube/Example.thy Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Cube/Example.thy Mon Mar 16 18:24:30 2009 +0100
@@ -15,20 +15,19 @@
*}
method_setup depth_solve = {*
- Method.thms_args (fn thms => METHOD (fn facts =>
- (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
+ Attrib.thms >> (fn thms => K (METHOD (fn facts =>
+ (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
*} ""
method_setup depth_solve1 = {*
- Method.thms_args (fn thms => METHOD (fn facts =>
- (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms))))))
+ Attrib.thms >> (fn thms => K (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 (fn facts =>
- REPEAT (resolve_tac [strip_b, strip_s] 1 THEN DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1))))
- end
+ 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)))))
*} ""