--- a/src/Pure/Thy/thy_output.ML Wed Mar 04 10:43:39 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Mar 04 10:45:52 2009 +0100
@@ -519,9 +519,9 @@
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
-fun output_ml ml src ctxt (txt, pos) =
+fun output_ml ml _ ctxt (txt, pos) =
(ML_Context.eval_in (SOME ctxt) false pos (ml txt);
- (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
+ SymbolPos.content (SymbolPos.explode (txt, pos))
|> (if ! quotes then quote else I)
|> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else