src/Doc/Codegen/Computations.thy

     "Rings.dvd :: int \<Rightarrow> int \<Rightarrow> bool"
     "plus :: int \<Rightarrow> int \<Rightarrow> int"
     "minus :: int \<Rightarrow> int \<Rightarrow> int"
     "times :: int \<Rightarrow> int \<Rightarrow> int"
     "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
-  } (curry dvd_oracle)
+  } (K (curry dvd_oracle))
 
   end
 \<close>
 
 text \<open>

 
   val cterm_of_int = Thm.cterm_of @{context} o HOLogic.mk_numeral o integer_of_int;
 
   val divisor = Thm.dest_arg o Thm.dest_arg;
 
-  fun evaluate thm = 
-    Simplifier.rewrite_rule 
-      (Proof_Context.transfer (Thm.theory_of_thm thm) @{context})
-      (map mk_eq @{thms arith_simps positive_mult}) thm; (*FIXME proper ctxt*)
-
-  fun revaluate k ct =
+  val evaluate_simps = map mk_eq @{thms arith_simps positive_mult};
+
+  fun evaluate ctxt = 
+    Simplifier.rewrite_rule ctxt evaluate_simps;
+
+  fun revaluate ctxt k ct =
     @{thm conv_div_cert}
     |> Thm.instantiate' [] [SOME (cterm_of_int k), SOME (divisor ct)]
-    |> evaluate;
+    |> evaluate ctxt;
 
   in
 
   val conv_div = @{computation_conv int terms:
     "divide :: int \<Rightarrow> int \<Rightarrow> int"