Attrib.pretty_attrib;
authorwenzelm
Sat Oct 14 23:25:51 2006 +0200 (2006-10-14)
changeset 21032a4b85340d6bd
parent 21031 a56e6d1e56a3
child 21033 82f44ceb4fa3
Attrib.pretty_attrib;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Sat Oct 14 23:25:50 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sat Oct 14 23:25:51 2006 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4  fun pretty_name_atts ctxt (name, atts) sep =
     1.5    if name = "" andalso null atts then []
     1.6    else [Pretty.block
     1.7 -    (Pretty.breaks (Pretty.str name :: Args.pretty_attribs ctxt atts @ [Pretty.str sep]))];
     1.8 +    (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
     1.9  
    1.10  
    1.11  (* pretty_stmt *)
    1.12 @@ -200,7 +200,7 @@
    1.13  
    1.14      fun prt_fact (ths, []) = map prt_thm ths
    1.15        | prt_fact (ths, atts) = Pretty.enclose "(" ")"
    1.16 -          (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts;
    1.17 +          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
    1.18      fun prt_note (a, ths) =
    1.19        Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
    1.20    in