# HG changeset patch
# User wenzelm
# Date 1752576008 -7200
# Node ID 9a19d83dfd5c0fcb1d7f62cd70e6326afd39993d
# Parent  9cdc0504aa2f3b25fce466e81dbcab5004823701
clarified signature: more uniform;

diff -r 9cdc0504aa2f -r 9a19d83dfd5c src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 15 12:37:50 2025 +0200
+++ b/src/Provers/classical.ML	Tue Jul 15 12:40:08 2025 +0200
@@ -285,10 +285,10 @@
 
 (* erros and warnings *)
 
-fun err_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
+fun err_thm ctxt msg th = error (msg () ^ "\n" ^ Thm.string_of_thm ctxt th);
 
 fun err_thm_illformed ctxt kind th =
-  err_thm ctxt ("Ill-formed " ^ Bires.kind_name kind) th;
+  err_thm ctxt (fn () => "Ill-formed " ^ Bires.kind_name kind) th;
 
 fun init_decl kind opt_weight info : decl =
   let val weight = the_default (Bires.kind_index kind) opt_weight
@@ -299,11 +299,11 @@
 
 fun warn_thm ctxt msg th =
   if Context_Position.is_really_visible ctxt
-  then warning (msg () ^ Thm.string_of_thm ctxt th) else ();
+  then warning (msg () ^ "\n" ^ Thm.string_of_thm ctxt th) else ();
 
 fun warn_kind ctxt decls prefix th kind =
   is_declared decls th kind andalso
-    (warn_thm ctxt (fn () => prefix ^ Bires.kind_description kind ^ "\n") th; true);
+    (warn_thm ctxt (fn () => prefix ^ Bires.kind_description kind) th; true);
 
 fun warn_other_kinds ctxt decls th =
   let val warn = warn_kind ctxt decls "Rule already declared as " th in
@@ -436,11 +436,11 @@
     val _ =
       if Bires.has_decls decls (Tactic.make_elim th) then
         warn_thm ctxt
-          (fn () => "Not deleting elim format --- need to to declare proper dest rule\n") th
+          (fn () => "Not deleting elim format --- need to to declare proper dest rule") th
       else ();
   in
     if null old_decls then
-      (if warn then warn_thm ctxt (fn () => "Undeclared classical rule\n") th else (); cs)
+      (if warn then warn_thm ctxt (fn () => "Undeclared classical rule") th else (); cs)
     else
       let
         fun del which ({tag = {index, ...}, info, ...}: decl) = delete_rl index (which info);