# HG changeset patch
# User wenzelm
# Date 1753031181 -7200
# Node ID e5db7672d1923dd1b0972b0467f6981e0d07a7a2
# Parent  8d1e295aab7080a8a1cc0ebd969372508c55bff7
more robust treatment of impossible case;

diff -r 8d1e295aab70 -r e5db7672d192 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jul 19 18:41:55 2025 +0200
+++ b/src/Provers/classical.ML	Sun Jul 20 19:06:21 2025 +0200
@@ -336,7 +336,7 @@
 fun add_rule (decl as {kind, ...}: decl) =
   if Bires.kind_safe kind then add_safe_rule decl
   else if Bires.kind_unsafe kind then add_unsafe_rule decl
-  else I;
+  else raise Fail "Bad rule kind";
 
 
 fun trim_context_rl (th1, opt_th2) =