# HG changeset patch
# User wenzelm
# Date 1571770797 -7200
# Node ID 15758fced053d46cb84fe2b4e58b3a59f0c88aef
# Parent  98d9b78b7f47de61a7369e3fd6c5530ca971a4e7
no printing of axioms -- too bulky;

diff -r 98d9b78b7f47 -r 15758fced053 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Oct 22 20:55:13 2019 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 22 20:59:57 2019 +0200
@@ -122,8 +122,6 @@
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
     val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
-
-    val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
   in
     Pretty.chunks
      [Pretty.big_list "classes:" (map pretty_classrel clsses),
@@ -134,7 +132,6 @@
       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
-      Pretty.big_list "axioms:" (map pretty_axm axms),
       Pretty.block
         (Pretty.breaks (Pretty.str "oracles:" ::
           map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]