--- a/src/Pure/Isar/isar_cmd.ML Sat May 15 22:24:25 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat May 15 23:16:32 2010 +0200
@@ -507,7 +507,7 @@
fun check_text (txt, pos) state =
(Position.report Markup.doc_source pos;
- ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos)));
+ ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
fun header_markup txt = Toplevel.keep (fn state =>
if Toplevel.is_toplevel state then check_text txt state