# HG changeset patch
# User wenzelm
# Date 1429197975 -7200
# Node ID 2ce2e0358e91ed635ef9e0d2b6c80be6db12216d
# Parent  73c2603427041657fdc2933f5ee2a0472d43a746
clarified document antiquotation: same check as in ML antiquotation;

diff -r 73c260342704 -r 2ce2e0358e91 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Apr 16 17:18:48 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Apr 16 17:26:15 2015 +0200
@@ -540,11 +540,7 @@
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
-fun pretty_theory ctxt (name, pos) =
-  (case find_first (fn thy => Context.theory_name thy = name)
-      (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
-    NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos)
-  | SOME thy => (Context_Position.report ctxt pos (Theory.get_markup thy); Pretty.str name));
+fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
 
 
 (* default output *)