src/Pure/Thy/thy_output.ML
changeset 30208 0abadde7b3fb
parent 29606 fedb8be05f24
child 30317 159bab53b40d
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 02 20:31:27 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 03 12:12:38 2009 +0100
     1.3 @@ -519,9 +519,9 @@
     1.4  fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
     1.5  fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
     1.6  
     1.7 -fun output_ml ml src ctxt (txt, pos) =
     1.8 +fun output_ml ml _ ctxt (txt, pos) =
     1.9   (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
    1.10 -  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
    1.11 +  SymbolPos.content (SymbolPos.explode (txt, pos))
    1.12    |> (if ! quotes then quote else I)
    1.13    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.14    else