1.1 --- a/src/Pure/Thy/thy_output.ML	Wed Sep 17 21:27:36 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Sep 17 21:27:38 2008 +0200
     1.3 @@ -507,7 +507,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.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
     1.8 + (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
     1.9    (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
    1.10    |> (if ! quotes then quote else I)
    1.11    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"