--- a/ProgTutorial/Recipes/Oracle.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy	Tue May 14 11:10:53 2019 +0200
@@ -60,7 +60,7 @@
   let
     fun trans t =
       (case t of
-        @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>
+        @{term "(=) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>
           Buffer.add " (" #>
           trans t #>
           Buffer.add "<=>" #> 
@@ -120,18 +120,18 @@
   To be able to use our oracle for Isar proofs, we wrap it into a tactic:
 *}
 
-ML %grayML{*val iff_oracle_tac =
+ML %grayML{*fun iff_oracle_tac ctxt =
   CSUBGOAL (fn (goal, i) => 
     (case try iff_oracle goal of
       NONE => no_tac
-    | SOME thm => rtac thm i))*}
+    | SOME thm => resolve_tac ctxt [thm] i))*}
 
 text {*
   and create a new method solely based on this tactic:
 *}
 
 method_setup iff_oracle = {*
-   Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))
+   Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt)))
 *} "Oracle-based decision procedure for chains of equivalences"
 
 text {*