--- a/src/Sequents/ILL.thy Mon Mar 16 17:51:24 2009 +0100
+++ b/src/Sequents/ILL.thy Mon Mar 16 18:24:30 2009 +0100
@@ -146,7 +146,7 @@
*}
method_setup best_lazy =
- {* Method.no_args (SIMPLE_METHOD' (best_tac lazy_cs)) *}
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
"lazy classical reasoning"
lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
@@ -282,10 +282,10 @@
method_setup best_safe =
- {* Method.no_args (SIMPLE_METHOD' (best_tac safe_cs)) *} ""
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
method_setup best_power =
- {* Method.no_args (SIMPLE_METHOD' (best_tac power_cs)) *} ""
+ {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
(* Some examples from Troelstra and van Dalen *)