changeset 19731 | 581cdbdbba9a |
parent 19585 | 70a1ce3b23ae |
child 19777 | 77929c3d2b74 |
--- 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 *)