# HG changeset patch
# User wenzelm
# Date 1014666610 -3600
# Node ID 279a3cf23a9871dd453b0485337f9ac05e0c2058
# Parent  a646d0467d811bc9a8c504cd5209b316b77a53a2
export eval_antiquote;

diff -r a646d0467d81 -r 279a3cf23a98 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Feb 25 20:49:05 2002 +0100
+++ b/src/Pure/Isar/isar_output.ML	Mon Feb 25 20:50:10 2002 +0100
@@ -18,6 +18,7 @@
   datatype markup = Markup | MarkupEnv | Verbatim
   val interest_level: int ref
   val modes: string list ref
+  val eval_antiquote: Scan.lexicon -> Toplevel.state -> string * Position.T -> string
   val parse_thy: (markup -> OuterLex.token list -> OuterLex.token * OuterLex.token list) ->
     Scan.lexicon -> Toplevel.transition list -> (OuterLex.token, 'a) Source.source ->
       (Toplevel.transition * (Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T