src/FOL/intprover.ML

--- a/src/FOL/intprover.ML	Sat Jul 05 15:03:26 2025 +0200
+++ b/src/FOL/intprover.ML	Sat Jul 05 15:53:52 2025 +0200
@@ -39,7 +39,7 @@
   (handles double negations).  Could instead rewrite by not_def as the first
   step of an intuitionistic proof.
 *)
-val safe_brls = sort (make_ord lessb)
+val safe_brls = sort Bires.subgoals_ord
     [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}),
       (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
       (true, @{thm conjE}), (true, @{thm exE}),
@@ -59,7 +59,7 @@
 
 (*0 subgoals vs 1 or more: the p in safep is for positive*)
 val (safe0_brls, safep_brls) =
-    List.partition (curry (op =) 0 o subgoals_of_brl) safe_brls;
+    List.partition Bires.no_subgoals safe_brls;
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
 fun safe_step_tac ctxt =