--- a/src/Doc/antiquote_setup.ML Tue Feb 25 14:34:18 2014 +0100
+++ b/src/Doc/antiquote_setup.ML Tue Feb 25 14:56:58 2014 +0100
@@ -156,8 +156,6 @@
val _ = List.app (Position.report pos) markup;
in true end;
-fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt));
-
fun check_tool (name, pos) =
let
fun tool dir =
@@ -213,18 +211,18 @@
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #>
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #>
entity_antiqs (can o Method.check_name) "" "method" #>
- entity_antiqs (thy_check Attrib.check) "" "attribute" #>
+ entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #>
entity_antiqs no_check "" "fact" #>
entity_antiqs no_check "" "variable" #>
entity_antiqs no_check "" "case" #>
- entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #>
- entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #>
+ entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #>
+ entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #>
entity_antiqs no_check "isatt" "setting" #>
entity_antiqs no_check "isatt" "system option" #>
entity_antiqs no_check "" "inference" #>
entity_antiqs no_check "isatt" "executable" #>
entity_antiqs (K check_tool) "isatool" "tool" #>
- entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN;
+ entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN;
end;