# HG changeset patch
# User wenzelm
# Date 1443204265 -7200
# Node ID 0b6217fda81b86f7867ac27f161a831570879648
# Parent  eb9522a9d9971b9bf18ce4045cbc622b2cd34a19
less redundant output;

diff -r eb9522a9d997 -r 0b6217fda81b src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Sep 25 19:54:51 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Sep 25 20:04:25 2015 +0200
@@ -12,10 +12,10 @@
   val pp_term: (unit -> theory) -> term -> Pretty.T
   val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
   val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
+  val pretty_theory: bool -> Proof.context -> Pretty.T
   val pretty_definitions: bool -> Proof.context -> Pretty.T
   val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
   val pretty_theorems: bool -> Proof.context -> Pretty.T list
-  val pretty_theory: bool -> Proof.context -> Pretty.T
   val string_of_rule: Proof.context -> string -> thm -> string
   val pretty_goal_header: thm -> Pretty.T
   val string_of_goal: Proof.context -> thm -> string
@@ -60,19 +60,6 @@
 
 (** theory content **)
 
-(* theorems and theory *)
-
-fun pretty_theorems_diff verbose prev_thys ctxt =
-  let
-    val pretty_fact = Proof_Context.pretty_fact ctxt;
-    val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
-    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
-    val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
-  in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
-
-fun pretty_theorems verbose ctxt =
-  pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt;
-
 fun pretty_theory verbose ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
@@ -138,8 +125,8 @@
 
     val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
   in
-    [Pretty.strs ("names:" :: Context.display_names thy)] @
-    [Pretty.big_list "classes:" (map pretty_classrel clsses),
+    Pretty.chunks
+     [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),
@@ -150,9 +137,22 @@
       Pretty.big_list "axioms:" (map pretty_axm axms),
       Pretty.block
         (Pretty.breaks (Pretty.str "oracles:" ::
-          map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))] @
-    pretty_theorems verbose ctxt
-  end |> Pretty.chunks;
+          map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
+  end;
+
+
+(* theorems *)
+
+fun pretty_theorems_diff verbose prev_thys ctxt =
+  let
+    val pretty_fact = Proof_Context.pretty_fact ctxt;
+    val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
+    val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
+    val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
+  in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
+
+fun pretty_theorems verbose ctxt =
+  pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt;
 
 
 (* definitions *)
diff -r eb9522a9d997 -r 0b6217fda81b src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Sep 25 19:54:51 2015 +0200
+++ b/src/Pure/context.ML	Fri Sep 25 20:04:25 2015 +0200
@@ -36,8 +36,6 @@
   val theory_id_name: theory_id -> string
   val theory_name: theory -> string
   val PureN: string
-  val display_name: theory_id -> string
-  val display_names: theory -> string list
   val pretty_thy: theory -> Pretty.T
   val string_of_thy: theory -> string
   val pretty_abbrev_thy: theory -> Pretty.T