# HG changeset patch
# User wenzelm
# Date 1236699839 -3600
# Node ID 6037cac149a1fc04775620a15f99cd4f5beda058
# Parent  d1fe8cea5db9ce49d7b9bd6ef9b246185f43fa63
pretty_full_theory: no longer display name prefix -- naming is far more complex now;

diff -r d1fe8cea5db9 -r 6037cac149a1 src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Mar 10 16:42:58 2009 +0100
+++ b/src/Pure/display.ML	Tue Mar 10 16:43:59 2009 +0100
@@ -213,8 +213,7 @@
     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.display_names thy)] @
-    [Pretty.strs ["name prefix:", NameSpace.path_of naming],
-      Pretty.big_list "classes:" (map pretty_classrel clsses),
+    [Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
       Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
       Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),