# HG changeset patch
# User wenzelm
# Date 1566056704 -7200
# Node ID f4d111b802a11b060035119da168f3faf05d59df
# Parent  fb3d06d7dd05c1eb8b913e8e5bf0deb7345952af
proper theory context for global props;

diff -r fb3d06d7dd05 -r f4d111b802a1 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 17 17:28:08 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 17 17:45:04 2019 +0200
@@ -27,9 +27,11 @@
 
 fun pretty_thm_oracles ctxt thms =
   let
+    val thy = Proof_Context.theory_of ctxt;
     fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name]
       | prt_oracle (name, SOME prop) =
-          [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, Syntax.pretty_term ctxt prop];
+          [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1,
+            Syntax.pretty_term_global thy prop];
   in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;