1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 24 18:44:21 2008 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 24 23:34:24 2008 +0100
     1.3 @@ -501,8 +501,8 @@
     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 =
     1.8 - (ML_Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
     1.9 +fun output_ml ml src ctxt (txt, pos) =
    1.10 + (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt));
    1.11    (if ! source then str_of_source src else txt)
    1.12    |> (if ! quotes then quote else I)
    1.13    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.14 @@ -531,8 +531,8 @@
    1.15    ("prf", args Attrib.thms (output (pretty_prf false))),
    1.16    ("full_prf", args Attrib.thms (output (pretty_prf true))),
    1.17    ("theory", args (Scan.lift Args.name) (output pretty_theory)),
    1.18 -  ("ML", args (Scan.lift Args.name) (output_ml ml_val)),
    1.19 -  ("ML_type", args (Scan.lift Args.name) (output_ml ml_type)),
    1.20 -  ("ML_struct", args (Scan.lift Args.name) (output_ml ml_struct))];
    1.21 +  ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
    1.22 +  ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
    1.23 +  ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
    1.24  
    1.25  end;