author | wenzelm |
Fri, 26 May 2006 22:20:05 +0200 | |
changeset 19731 | 581cdbdbba9a |
parent 19730 | 8abecd308e60 |
child 19732 | 1c37d117a25d |
--- a/src/Pure/Isar/element.ML Fri May 26 22:20:05 2006 +0200 +++ b/src/Pure/Isar/element.ML Fri May 26 22:20:05 2006 +0200 @@ -236,8 +236,8 @@ fun pretty_name_atts ctxt (name, atts) sep = if name = "" andalso null atts then [] - else [Pretty.block (Pretty.breaks (Pretty.str (ProofContext.extern_thm ctxt name) :: - Args.pretty_attribs ctxt atts @ [Pretty.str sep]))]; + else [Pretty.block + (Pretty.breaks (Pretty.str name :: Args.pretty_attribs ctxt atts @ [Pretty.str sep]))]; (* pretty_stmt *)