# HG changeset patch
# User wenzelm
# Date 1176493109 -7200
# Node ID 2d4d02efd9d95212157a2a78e3264faeb40edca1
# Parent  cf152ff55d162d4652dbf3d2b51bff41316c3129
added eval_antiquotes_fn (tmp);

diff -r cf152ff55d16 -r 2d4d02efd9d9 src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Fri Apr 13 21:26:35 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Fri Apr 13 21:38:29 2007 +0200
@@ -31,6 +31,7 @@
     (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
   val proj_value_antiq: string -> (Context.generic * Args.T list ->
       (string * string * string) * (Context.generic * Args.T list)) -> unit
+  val eval_antiquotes_fn: (string -> string * string) ref  (* FIXME tmp *)
   val use_mltext: string -> bool -> Context.generic option -> unit
   val use_mltext_update: string -> bool -> Context.generic -> Context.generic
   val use_let: string -> string -> string -> Context.generic -> Context.generic
@@ -164,9 +165,11 @@
 
 in
 
+val eval_antiquotes_fn = ref eval_antiquotes;
+
 fun eval_wrapper name verbose txt =
   let
-    val (txt1, txt2) = eval_antiquotes txt;
+    val (txt1, txt2) = ! eval_antiquotes_fn txt;
     val _ =
       if txt1 = isabelle_struct0 andalso txt2 = txt then ()
       else Output.debug (fn () => cat_lines [txt1, txt2]);