diff -r df09e49b19bf -r 733614e236a3 CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Wed Sep 17 19:20:37 2008 -0400
+++ b/CookBook/antiquote_setup.ML	Tue Sep 30 03:30:40 2008 -0400
@@ -1,5 +1,5 @@
 (*  Title:      Doc/antiquote_setup.ML
-    ID:         $Id: antiquote_setup.ML,v 1.30 2008/09/16 12:39:56 wenzelm Exp $
+    ID:         $Id: antiquote_setup.ML,v 1.32 2008/09/29 10:31:56 haftmann Exp $
     Author:     Makarius
 
 Auxiliary antiquotations for the Isabelle manuals.
@@ -75,7 +75,7 @@
       else txt1 ^ ": " ^ txt2;
     val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     val _ = writeln (ml (txt1, txt2));
-    val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
+    val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
   in
     "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
     ((if ! O.source then str_of_source src else txt')
@@ -205,7 +205,8 @@
   entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
   entity_antiqs no_check "isatt" "executable" @
   entity_antiqs (K check_tool) "isatt" "tool" @
-  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file");
+  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
+  entity_antiqs (K ThyInfo.known_thy) "" "theory");
 
 end;