doc-src/antiquote_setup.ML

   let val thy = Proof_Context.theory_of ctxt
   in defined thy o intern thy end;
 
 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 =
   Thy_Output.antiquotation

     "" "antiquotation option" #>
   entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" #>
   entity_antiqs no_check "" "inference" #>
   entity_antiqs no_check "isatt" "executable" #>
   entity_antiqs (K check_tool) "isatt" "tool" #>
-  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;
 
 end;