Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Codegen/Computations.thy
changeset 78795 f7e972d567f3
parent 76987 4c275405faae 
--- a/src/Doc/Codegen/Computations.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Doc/Codegen/Computations.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -276,8 +276,7 @@
     \<^instantiate>\<open>x = ct and y = \<open>if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>\<close>
       in cterm \<open>x \<equiv> y\<close> for x y :: bool\<close>;
 
-  val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
-    (Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd)));
+  val (_, dvd_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd));
 
   in
isabelle