minor performance tuning;

--- a/src/Provers/classical.ML	Sat Jul 05 15:53:52 2025 +0200
+++ b/src/Provers/classical.ML	Sat Jul 05 16:01:40 2025 +0200
@@ -337,7 +337,7 @@
     let
       val (th, rl, _) = r;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
-        List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl];
+        List.partition (Thm.one_prem o #1) [rl];
       val nI = Item_Net.length safeIs;
       val nE = Item_Net.length safeEs + 1;
     in
@@ -485,7 +485,7 @@
     safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) =
   let
     val (th, rl, _) = r;
-    val (safe0_rls, safep_rls) = List.partition (fn (rl, _) => Thm.nprems_of rl = 1) [rl];
+    val (safe0_rls, safep_rls) = List.partition (Thm.one_prem o #1) [rl];
   in
     CS
      {safe0_netpair = delete ([], map fst safe0_rls) safe0_netpair,

--- a/src/Pure/bires.ML	Sat Jul 05 15:53:52 2025 +0200
+++ b/src/Pure/bires.ML	Sat Jul 05 16:01:40 2025 +0200
@@ -41,7 +41,8 @@
 
 val subgoals_ord = int_ord o apply2 subgoals_of;
 
-fun no_subgoals rl = subgoals_of rl = 0;
+fun no_subgoals (true, thm) = Thm.one_prem thm
+  | no_subgoals (false, thm) = Thm.no_prems thm;
 
 
 (** To preserve the order of the rules, tag them with increasing integers **)

--- a/src/Pure/goal.ML	Sat Jul 05 15:53:52 2025 +0200
+++ b/src/Pure/goal.ML	Sat Jul 05 16:01:40 2025 +0200
@@ -268,7 +268,7 @@
 
 (*with structural marker*)
 fun SELECT_GOAL tac i st =
-  if Thm.nprems_of st = 1 andalso i = 1 then tac st
+  if Thm.one_prem st andalso i = 1 then tac st
   else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st;
 
 (*without structural marker*)

--- a/src/Pure/logic.ML	Sat Jul 05 15:53:52 2025 +0200
+++ b/src/Pure/logic.ML	Sat Jul 05 16:01:40 2025 +0200
@@ -27,6 +27,7 @@
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
   val no_prems: term -> bool
+  val one_prem: term -> bool
   val nth_prem: int * term -> term
   val close_term: (string * term) list -> term -> term
   val close_prop: (string * term) list -> term list -> term -> term
@@ -221,6 +222,9 @@
 fun no_prems (Const ("Pure.imp", _) $ _ $ _) = false
   | no_prems _ = true;
 
+fun one_prem (Const ("Pure.imp", _) $ _ $ B) = no_prems B
+  | one_prem _ = false;
+
 (*Select Ai from A1\<Longrightarrow>...Ai\<Longrightarrow>B*)
 fun nth_prem (1, Const ("Pure.imp", _) $ A $ _) = A
   | nth_prem (i, Const ("Pure.imp", _) $ _ $ B) = nth_prem (i - 1, B)

--- a/src/Pure/thm.ML	Sat Jul 05 15:53:52 2025 +0200
+++ b/src/Pure/thm.ML	Sat Jul 05 16:01:40 2025 +0200
@@ -82,6 +82,7 @@
   val take_prems_of: int -> thm -> term list
   val nprems_of: thm -> int
   val no_prems: thm -> bool
+  val one_prem: thm -> bool
   val prem_of: thm -> int -> term
   val major_prem_of: thm -> term
   val cprop_of: thm -> cterm
@@ -532,6 +533,7 @@
 fun take_prems_of n = Logic.take_imp_prems n o prop_of;
 val nprems_of = Logic.count_prems o prop_of;
 val no_prems = Logic.no_prems o prop_of;
+val one_prem = Logic.one_prem o prop_of;
 
 fun prem_of th i =
   Logic.nth_prem (i, prop_of th) handle TERM _ => raise THM ("prem_of", i, [th]);