# HG changeset patch
# User haftmann
# Date 1329592067 -3600
# Node ID 11b6471c2f50c46cf07fce27e0703df0404a0a5b
# Parent  9d2e682a68eb30395cae18f5a794a708d5344b4e
more precise semantics of "theory" antiquotation

diff -r 9d2e682a68eb -r 11b6471c2f50 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sat Feb 18 20:07:26 2012 +0100
+++ b/doc-src/antiquote_setup.ML	Sat Feb 18 20:07:47 2012 +0100
@@ -151,6 +151,9 @@
 fun check_tool name =
   File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
 
+fun is_ancestor thy name =
+  exists (fn thy => Context.theory_name thy = name) (thy :: Context.ancestors_of thy);
+
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup kind index =
@@ -207,7 +210,7 @@
   entity_antiqs no_check "" "inference" #>
   entity_antiqs no_check "isatt" "executable" #>
   entity_antiqs (K check_tool) "isatt" "tool" #>
-  entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #>
+  entity_antiqs (is_ancestor o Proof_Context.theory_of) "" "theory" #>
   entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
     "" Isabelle_Markup.ML_antiquotationN;