Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust treatment of impossible case;
authorwenzelm
Sun, 20 Jul 2025 19:06:21 +0200
changeset 82887 e5db7672d192
parent 82886 8d1e295aab70
child 82888 051177553f16
more robust treatment of impossible case;
src/Provers/classical.ML file | annotate | diff | comparison | revisions 
--- 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) =
isabelle