CookBook/Recipes/Oracle.thy
changeset 181 5baaabe1ab92
parent 154 e81ebb37aa83
--- a/CookBook/Recipes/Oracle.thy	Tue Mar 17 01:56:29 2009 +0100
+++ b/CookBook/Recipes/Oracle.thy	Tue Mar 17 11:47:01 2009 +0100
@@ -133,12 +133,10 @@
 *}
 
 method_setup iff_oracle = {*
-   Method.no_args (Method.SIMPLE_METHOD' iff_oracle_tac)
+   Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))
 *} "Oracle-based decision procedure for chains of equivalences"
 
 text {*
-  (FIXME: what does @{ML "Method.SIMPLE_METHOD'"} do? ... what do you mean?)
-
   Finally, we can test our oracle to prove some theorems:
 *}