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/Tools/nbe.ML
changeset 78795 f7e972d567f3
parent 77707 a6a81f848135 
--- a/src/Tools/nbe.ML	Tue Oct 17 22:29:12 2023 +0200
+++ b/src/Tools/nbe.ML	Wed Oct 18 15:13:52 2023 +0200
@@ -78,9 +78,9 @@
 
 val get_triv_classes = map fst o Triv_Class_Data.get;
 
-val (_, triv_of_class) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>triv_of_class\<close>, fn (thy, T, class) =>
-    Thm.global_cterm_of thy (Logic.mk_of_class (T, class)))));
+val (_, triv_of_class) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>triv_of_class\<close>,
+    fn (thy, T, class) => Thm.global_cterm_of thy (Logic.mk_of_class (T, class))));
 
 in
 
@@ -592,10 +592,10 @@
     val rhs = Thm.cterm_of ctxt raw_rhs;
   in Thm.mk_binop eq lhs rhs end;
 
-val (_, raw_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (\<^binding>\<open>normalization_by_evaluation\<close>,
+val (_, raw_oracle) =
+  Theory.setup_result (Thm.add_oracle (\<^binding>\<open>normalization_by_evaluation\<close>,
     fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
-      mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
+      mk_equals ctxt ct (normalize_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps)));
 
 fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
   raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);
isabelle