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/HOL/Decision_Procs/Reflective_Field.thy
changeset 78795 f7e972d567f3
parent 78096 838198d17a40 
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Wed Oct 18 15:13:52 2023 +0200
@@ -643,8 +643,7 @@
   \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt t\<close>
     in cterm \<open>x \<equiv> y\<close> for x y :: \<open>pexpr \<times> pexpr \<times> pexpr list\<close>\<close>;
 
-val (_, raw_fnorm_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm)));
+val (_, raw_fnorm_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>\<open>fnorm\<close>, fnorm));
 
 fun fnorm_oracle ctxt ct t = raw_fnorm_oracle (ctxt, ct, t);
isabelle