Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pretty_full_theory: no longer display name prefix -- naming is far more complex now;
authorwenzelm
Tue, 10 Mar 2009 16:43:59 +0100
changeset 30409 6037cac149a1
parent 30408 d1fe8cea5db9
child 30410 ef670320e281
pretty_full_theory: no longer display name prefix -- naming is far more complex now;
src/Pure/display.ML file | annotate | diff | comparison | revisions 
--- 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),
isabelle