# HG changeset patch
# User wenzelm
# Date 962473246 -7200
# Node ID 50de4abb987c0fcea5d72e9094ac6e0f716b01bb
# Parent  9454f30eacc709439b929252112793e8ac933c1d
print_theorems: omit name space;

diff -r 9454f30eacc7 -r 50de4abb987c src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat Jul 01 17:52:52 2000 +0200
+++ b/src/Pure/pure_thy.ML	Sat Jul 01 19:40:46 2000 +0200
@@ -86,12 +86,9 @@
         | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
 
       val thmss = NameSpace.cond_extern_table space thms_tab;
-    in
-      [Display.pretty_name_space ("theorem name space", space),
-        Pretty.big_list "theorems:" (map prt_thms thmss)]
-    end;
+    in Pretty.big_list "theorems:" (map prt_thms thmss) end;
 
-  fun print sg data = Pretty.writeln (Pretty.chunks (pretty sg data));
+  fun print sg data = Pretty.writeln (pretty sg data);
 end;
 
 structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
@@ -106,7 +103,8 @@
 val print_theorems = TheoremsData.print;
 
 fun print_theory thy =
-  Display.pretty_full_theory thy @ TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)
+  Display.pretty_full_theory thy @
+  [TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)]
   |> Pretty.chunks |> Pretty.writeln;