# HG changeset patch
# User wenzelm
# Date 1160861151 -7200
# Node ID a4b85340d6bdf7019a48b9c83ccfce79c8c2c527
# Parent  a56e6d1e56a3a5178d9b8d3e49ed24f03bff48c5
Attrib.pretty_attrib;

diff -r a56e6d1e56a3 -r a4b85340d6bd src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Oct 14 23:25:50 2006 +0200
+++ b/src/Pure/Isar/element.ML	Sat Oct 14 23:25:51 2006 +0200
@@ -148,7 +148,7 @@
 fun pretty_name_atts ctxt (name, atts) sep =
   if name = "" andalso null atts then []
   else [Pretty.block
-    (Pretty.breaks (Pretty.str name :: Args.pretty_attribs ctxt atts @ [Pretty.str sep]))];
+    (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
 
 
 (* pretty_stmt *)
@@ -200,7 +200,7 @@
 
     fun prt_fact (ths, []) = map prt_thm ths
       | prt_fact (ths, atts) = Pretty.enclose "(" ")"
-          (Pretty.breaks (map prt_thm ths)) :: Args.pretty_attribs ctxt atts;
+          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
     fun prt_note (a, ths) =
       Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
   in