1.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 14 21:06:07 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Aug 15 15:50:44 2008 +0200
     1.3 @@ -508,7 +508,7 @@
     1.4  
     1.5  fun output_ml ml src ctxt (txt, pos) =
     1.6   (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
     1.7 -  (if ! source then str_of_source src else txt)
     1.8 +  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
     1.9    |> (if ! quotes then quote else I)
    1.10    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.11    else
    1.12 @@ -545,7 +545,7 @@
    1.13    ("term_type", args Args.term (output pretty_term_typ)),
    1.14    ("typeof", args Args.term (output pretty_term_typeof)),
    1.15    ("const", args Args.const_proper (output pretty_const)),
    1.16 -  ("abbrev", args (Scan.lift Args.name) (output pretty_abbrev)),
    1.17 +  ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
    1.18    ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
    1.19    ("text", args (Scan.lift Args.name) (output (K pretty_text))),
    1.20    ("goals", output_goals true),
    1.21 @@ -553,8 +553,8 @@
    1.22    ("prf", args Attrib.thms (output (pretty_prf false))),
    1.23    ("full_prf", args Attrib.thms (output (pretty_prf true))),
    1.24    ("theory", args (Scan.lift Args.name) (output pretty_theory)),
    1.25 -  ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
    1.26 -  ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
    1.27 -  ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
    1.28 +  ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
    1.29 +  ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
    1.30 +  ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
    1.31  
    1.32  end;