1.1 --- a/doc-src/antiquote_setup.ML Sat Feb 18 20:07:26 2012 +0100
1.2 +++ b/doc-src/antiquote_setup.ML Sat Feb 18 20:07:47 2012 +0100
1.3 @@ -151,6 +151,9 @@
1.4 fun check_tool name =
1.5 File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
1.6
1.7 +fun is_ancestor thy name =
1.8 + exists (fn thy => Context.theory_name thy = name) (thy :: Context.ancestors_of thy);
1.9 +
1.10 val arg = enclose "{" "}" o clean_string;
1.11
1.12 fun entity check markup kind index =
1.13 @@ -207,7 +210,7 @@
1.14 entity_antiqs no_check "" "inference" #>
1.15 entity_antiqs no_check "isatt" "executable" #>
1.16 entity_antiqs (K check_tool) "isatt" "tool" #>
1.17 - entity_antiqs (K (can Thy_Info.get_theory)) "" "theory" #>
1.18 + entity_antiqs (is_ancestor o Proof_Context.theory_of) "" "theory" #>
1.19 entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
1.20 "" Isabelle_Markup.ML_antiquotationN;
1.21