pretty_full_theory: no longer display name prefix -- naming is far more complex now;
authorwenzelm
Tue Mar 10 16:43:59 2009 +0100 (2009-03-10)
changeset 304096037cac149a1
parent 30408 d1fe8cea5db9
child 30410 ef670320e281
pretty_full_theory: no longer display name prefix -- naming is far more complex now;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Tue Mar 10 16:42:58 2009 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Mar 10 16:43:59 2009 +0100
     1.3 @@ -213,8 +213,7 @@
     1.4      val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
     1.5    in
     1.6      [Pretty.strs ("names:" :: Context.display_names thy)] @
     1.7 -    [Pretty.strs ["name prefix:", NameSpace.path_of naming],
     1.8 -      Pretty.big_list "classes:" (map pretty_classrel clsses),
     1.9 +    [Pretty.big_list "classes:" (map pretty_classrel clsses),
    1.10        pretty_default default,
    1.11        Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
    1.12        Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),