# 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);