1.1 --- a/src/Pure/Thy/thy_output.ML Thu Mar 27 21:49:10 2008 +0100
1.2 +++ b/src/Pure/Thy/thy_output.ML Fri Mar 28 00:02:54 2008 +0100
1.3 @@ -502,7 +502,7 @@
1.4 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
1.5
1.6 fun output_ml ml src ctxt (txt, pos) =
1.7 - (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt));
1.8 + (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
1.9 (if ! source then str_of_source src else txt)
1.10 |> (if ! quotes then quote else I)
1.11 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"