avoid redefinition of @{theory} antiquotation
authorhaftmann
Sat Feb 18 20:50:11 2012 +0100 (2012-02-18)
changeset 465248d51b375e926
parent 46523 7ca897381b26
child 46525 af3df09590f9
avoid redefinition of @{theory} antiquotation
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Sat Feb 18 20:13:38 2012 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Sat Feb 18 20:50:11 2012 +0100
     1.3 @@ -151,9 +151,6 @@
     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 @@ -210,7 +207,6 @@
    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 (is_ancestor o Proof_Context.theory_of) "" "theory" #>
    1.18    entity_antiqs (thy_check ML_Context.intern_antiq ML_Context.defined_antiq)
    1.19      "" Isabelle_Markup.ML_antiquotationN;
    1.20