# HG changeset patch
# User wenzelm
# Date 1184102987 -7200
# Node ID a4af559708abe3fa631c68f6dca35c3775d2c256
# Parent  aa088ef9237cd911f67c2aa9991ebf3f0741cebb
export get_lexicons;

diff -r aa088ef9237c -r a4af559708ab src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 10 23:29:46 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 10 23:29:47 2007 +0200
@@ -26,6 +26,7 @@
   include BASIC_OUTER_SYNTAX
   type token
   type parser
+  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val command: string -> string -> OuterKeyword.T ->
     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
   val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->