--- a/src/Doc/Codegen/Computations.thy Mon Oct 25 20:38:58 2021 +0200
+++ b/src/Doc/Codegen/Computations.thy Mon Oct 25 21:31:35 2021 +0200
@@ -272,8 +272,9 @@
ML %quote \<open>
local
- fun raw_dvd (b, ct) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop\<close>
- ct (if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>);
+ fun raw_dvd (b, ct) =
+ \<^instantiate>\<open>x = ct and y = \<open>if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>\<close>
+ in cterm "x \<equiv> y" for x y :: bool\<close>;
val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd)));
--- a/src/HOL/ex/Sorting_Algorithms_Examples.thy Mon Oct 25 20:38:58 2021 +0200
+++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy Mon Oct 25 21:31:35 2021 +0200
@@ -23,8 +23,9 @@
val term_of_int_list = HOLogic.mk_list \<^typ>\<open>int\<close>
o map (HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int});
- fun raw_sort (ctxt, ct, ks) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop\<close>
- ct (Thm.cterm_of ctxt (term_of_int_list ks));
+ fun raw_sort (ctxt, ct, ks) =
+ \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt (term_of_int_list ks)\<close>
+ in cterm "x \<equiv> y" for x y :: "int list"\<close>;
val (_, sort_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort)));