# HG changeset patch
# User wenzelm
# Date 1752484690 -7200
# Node ID 2703f19d323e08e92c787e060fc9c8e11596c88d
# Parent  af6f55b15749f409dbfd5e077de4651dbaeb8a5f
clarified output;

diff -r af6f55b15749 -r 2703f19d323e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Jul 14 10:57:46 2025 +0200
+++ b/src/Provers/classical.ML	Mon Jul 14 11:18:10 2025 +0200
@@ -867,13 +867,10 @@
 fun print_claset ctxt =
   let
     val {decls, swrappers, uwrappers, ...} = rep_claset_of ctxt;
-    val prt_rules =
-      Bires.pretty_decls ctxt
-        [Bires.intro_bang_kind, Bires.intro_kind, Bires.elim_bang_kind, Bires.elim_kind] decls;
     val prt_wrappers =
      [Pretty.strs ("safe wrappers:" :: map #1 swrappers),
       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)];
-  in Pretty.writeln (Pretty.chunks (prt_rules @ prt_wrappers)) end;
+  in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls @ prt_wrappers)) end;
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_claset\<close> "print context of Classical Reasoner"
diff -r af6f55b15749 -r 2703f19d323e src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Mon Jul 14 10:57:46 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Mon Jul 14 11:18:10 2025 +0200
@@ -113,7 +113,7 @@
 
 fun print_rules ctxt =
   let val Rules {decls, ...} = Data.get (Context.Proof ctxt)
-  in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt Bires.kind_domain decls)) end;
+  in Pretty.writeln (Pretty.chunks (Bires.pretty_decls ctxt decls)) end;
 
 
 (* access data *)
diff -r af6f55b15749 -r 2703f19d323e src/Pure/bires.ML
--- a/src/Pure/bires.ML	Mon Jul 14 10:57:46 2025 +0200
+++ b/src/Pure/bires.ML	Mon Jul 14 11:18:10 2025 +0200
@@ -47,7 +47,7 @@
   val has_decls: 'a decls -> thm -> bool
   val get_decls: 'a decls -> thm -> 'a decl list
   val dest_decls: 'a decls -> (thm * 'a decl -> bool) -> (thm * 'a decl) list
-  val pretty_decls: Proof.context -> kind list -> 'a decls -> Pretty.T list
+  val pretty_decls: Proof.context -> 'a decls -> Pretty.T list
   val merge_decls: 'a decls * 'a decls -> 'a decl list * 'a decls
   val extend_decls: thm * 'a decl -> 'a decls -> 'a decl option * 'a decls
   val remove_decls: thm -> 'a decls -> 'a decl list * 'a decls
@@ -120,8 +120,8 @@
 val kind_infos =
  [(intro_bang_kind, ("safe introduction", "(intro!)")),
   (elim_bang_kind, ("safe elimination", "(elim!)")),
-  (intro_kind, ("introduction", "(intro)")),
-  (elim_kind, ("elimination", "(elim)")),
+  (intro_kind, ("unsafe introduction", "(intro)")),
+  (elim_kind, ("unsafe elimination", "(elim)")),
   (intro_query_kind, ("extra introduction", "(intro?)")),
   (elim_query_kind, ("extra elimination", "(elim?)"))];
 
@@ -189,11 +189,13 @@
   build (rules |> Proptab.fold (fn (th, ds) => ds |> fold (fn d => pred (th, d) ? cons (th, d))))
   |> sort (decl_ord o apply2 #2);
 
-fun pretty_decls ctxt kinds decls =
-  kinds |> map (fn kind =>
-    Pretty.big_list (kind_title kind ^ ":")
-      (dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind')
-        |> map (fn (th, _) => Thm.pretty_thm_item ctxt th)));
+fun pretty_decls ctxt decls =
+  kind_domain |> map_filter (fn kind =>
+    (case dest_decls decls (fn (_, {kind = kind', ...}) => kind = kind') of
+      [] => NONE
+    | ds =>
+        SOME (Pretty.big_list (kind_title kind ^ ":")
+          (map (Thm.pretty_thm_item ctxt o #1) ds))));
 
 fun merge_decls (decls1, decls2) =
   decls1 |> fold_map add_decls (rev (dest_decls decls2 (not o dup_decls decls1)));