# HG changeset patch
# User wenzelm
# Date 1751549311 -7200
# Node ID 070585eb5d5441fc4c641eb8b58c85cf2956359e
# Parent  c8d92d4ced73ea76b90b9fc18499d9f183c16b31
minor performance tuning;

diff -r c8d92d4ced73 -r 070585eb5d54 src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOL/ex/Prolog.thy	Thu Jul 03 15:28:31 2025 +0200
@@ -64,7 +64,7 @@
 (*backtracking version*)
 ML \<open>
 fun prolog_tac ctxt =
-  DEPTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt @{thms rules} 1)
+  DEPTH_FIRST Thm.no_prems (resolve_tac ctxt @{thms rules} 1)
 \<close>
 
 schematic_goal \<open>rev(?x, a:b:c:Nil)\<close>
diff -r c8d92d4ced73 -r 070585eb5d54 src/FOL/intprover.ML
--- a/src/FOL/intprover.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOL/intprover.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -90,11 +90,11 @@
 
 (*Slower but smarter than fast_tac*)
 fun best_tac ctxt =
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1));
 
 (*Uses all_dupE: allows multiple use of universal assumptions.  VERY slow.*)
 fun best_dup_tac ctxt =
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_dup_tac ctxt 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_dup_tac ctxt 1));
 
 
 end;
diff -r c8d92d4ced73 -r 070585eb5d54 src/FOLP/classical.ML
--- a/src/FOLP/classical.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOLP/classical.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -174,7 +174,7 @@
 
 (*Slower but smarter than fast_tac*)
 fun best_tac ctxt cs = 
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, sizef) (step_tac ctxt cs 1));
 
 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   allows backtracking from "safe" rules to "unsafe" rules here.*)
diff -r c8d92d4ced73 -r 070585eb5d54 src/FOLP/intprover.ML
--- a/src/FOLP/intprover.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/FOLP/intprover.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -72,6 +72,6 @@
 
 (*Slower but smarter than fast_tac*)
 fun best_tac ctxt =
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1));
 
 end;
diff -r c8d92d4ced73 -r 070585eb5d54 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -588,7 +588,7 @@
             (fn ctxt =>
               resolve_tac ctxt [exI] 1 THEN
               resolve_tac ctxt @{thms CollectI} 1 THEN
-              QUIET_BREADTH_FIRST (has_fewer_prems 1)
+              QUIET_BREADTH_FIRST Thm.no_prems
               (resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) =>
         let
           val permT = mk_permT
diff -r c8d92d4ced73 -r 070585eb5d54 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -603,7 +603,7 @@
     val pulled_tac_result = Seq.pull tac_result
     val tac_failed =
       is_none pulled_tac_result orelse
-       not (has_fewer_prems 1 (fst (the pulled_tac_result)))
+       not (Thm.no_prems (fst (the pulled_tac_result)))
   in
     if tac_failed then (wittler THEN' ASAP wittler tac) i st
     else tac_result
diff -r c8d92d4ced73 -r 070585eb5d54 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -685,10 +685,10 @@
   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
 
 fun best_prolog_tac ctxt sizef horns =
-    BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac ctxt horns 1);
+    BEST_FIRST (Thm.no_prems, sizef) (prolog_step_tac ctxt horns 1);
 
 fun depth_prolog_tac ctxt horns =
-    DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac ctxt horns 1);
+    DEPTH_FIRST Thm.no_prems (prolog_step_tac ctxt horns 1);
 
 (*Return all negative clauses, as possible goal clauses*)
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
@@ -717,7 +717,7 @@
   MESON all_tac (make_clauses ctxt)
     (fn cls =>
          THEN_BEST_FIRST (resolve_tac ctxt (gocls cls) 1)
-                         (has_fewer_prems 1, sizef)
+                         (Thm.no_prems, sizef)
                          (prolog_step_tac ctxt (make_horns cls) 1))
     ctxt
 
@@ -746,7 +746,7 @@
     end;
 
 fun iter_deepen_prolog_tac ctxt horns =
-    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' ctxt horns);
+    ITER_DEEPEN iter_deepen_limit Thm.no_prems (prolog_step_tac' ctxt horns);
 
 fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON all_tac (make_clauses ctxt)
   (fn cls =>
@@ -761,7 +761,7 @@
               ["clauses:"] @ map (Thm.string_of_thm ctxt) horns))
         in
           THEN_ITER_DEEPEN iter_deepen_limit
-            (resolve_tac ctxt goes 1) (has_fewer_prems 1) (prolog_step_tac' ctxt horns)
+            (resolve_tac ctxt goes 1) Thm.no_prems (prolog_step_tac' ctxt horns)
         end));
 
 fun meson_tac ctxt ths =
diff -r c8d92d4ced73 -r 070585eb5d54 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Provers/classical.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -287,7 +287,7 @@
 fun bad_thm ctxt msg th = error (msg ^ "\n" ^ Thm.string_of_thm ctxt th);
 
 fun make_elim ctxt th =
-  if has_fewer_prems 1 th then bad_thm ctxt "Ill-formed destruction rule" th
+  if Thm.no_prems th then bad_thm ctxt "Ill-formed destruction rule" th
   else Tactic.make_elim th;
 
 fun warn_thm ctxt msg th =
@@ -423,7 +423,7 @@
 
 fun addSE w ctxt th (cs as CS {safeEs, ...}) =
   let
-    val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
+    val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th;
     val th' = classical_rule ctxt (flat_rule ctxt th);
     val rl = (th', []);
     val r = trim_context (th, rl, rl);
@@ -446,7 +446,7 @@
 
 fun addE w ctxt th (cs as CS {unsafeEs, ...}) =
   let
-    val _ = has_fewer_prems 1 th andalso bad_thm ctxt "Ill-formed elimination rule" th;
+    val _ = Thm.no_prems th andalso bad_thm ctxt "Ill-formed elimination rule" th;
     val th' = classical_rule ctxt (flat_rule ctxt th);
     val dup_th' = dup_elim ctxt th' handle THM _ => bad_thm ctxt "Ill-formed elimination rule" th;
     val r = trim_context (th, (th', []), (dup_th', []));
@@ -804,12 +804,12 @@
 (*Slower but smarter than fast_tac*)
 fun best_tac ctxt =
   Object_Logic.atomize_prems_tac ctxt THEN'
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (step_tac ctxt 1));
 
 (*even a bit smarter than best_tac*)
 fun first_best_tac ctxt =
   Object_Logic.atomize_prems_tac ctxt THEN'
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
 
 fun slow_tac ctxt =
   Object_Logic.atomize_prems_tac ctxt THEN'
@@ -817,7 +817,7 @@
 
 fun slow_best_tac ctxt =
   Object_Logic.atomize_prems_tac ctxt THEN'
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, Data.sizef) (slow_step_tac ctxt 1));
 
 
 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
@@ -827,13 +827,13 @@
 fun astar_tac ctxt =
   Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL
-    (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
+    (ASTAR (Thm.no_prems, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
       (step_tac ctxt 1));
 
 fun slow_astar_tac ctxt =
   Object_Logic.atomize_prems_tac ctxt THEN'
   SELECT_GOAL
-    (ASTAR (has_fewer_prems 1, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
+    (ASTAR (Thm.no_prems, fn lev => fn thm => Data.sizef thm + weight_ASTAR * lev)
       (slow_step_tac ctxt 1));
 
 
diff -r c8d92d4ced73 -r 070585eb5d54 src/Pure/search.ML
--- a/src/Pure/search.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Pure/search.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -52,10 +52,10 @@
 fun has_fewer_prems n rule = Thm.nprems_of rule < n;
 
 (*Apply a tactic if subgoals remain, else do nothing.*)
-val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
+val IF_UNSOLVED = COND Thm.no_prems all_tac;
 
 (*Force a tactic to solve its goal completely, otherwise fail *)
-fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
+fun SOLVE tac = tac THEN COND Thm.no_prems all_tac no_tac;
 
 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
@@ -72,7 +72,7 @@
   | n => DEPTH_FIRST (has_fewer_prems n) tac);
 
 (*Uses depth-first search to solve ALL subgoals*)
-val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
+val DEPTH_SOLVE = DEPTH_FIRST Thm.no_prems;
 
 
 
diff -r c8d92d4ced73 -r 070585eb5d54 src/Sequents/modal.ML
--- a/src/Sequents/modal.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Sequents/modal.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -83,7 +83,7 @@
   rewrite_goals_tac ctxt Modal_Rule.rewrite_rls THEN solven_tac ctxt d 1;
 
 fun step_tac ctxt n =
-  COND (has_fewer_prems 1) all_tac
+  COND Thm.no_prems all_tac
        (DETERM(fres_safe_tac ctxt n) ORELSE
         (fres_unsafe_tac ctxt n APPEND fres_bound_tac ctxt n));
 
diff -r c8d92d4ced73 -r 070585eb5d54 src/Sequents/prover.ML
--- a/src/Sequents/prover.ML	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/Sequents/prover.ML	Thu Jul 03 15:28:31 2025 +0200
@@ -223,7 +223,7 @@
   SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 fun best_tac ctxt  =
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac ctxt 1));
+  SELECT_GOAL (BEST_FIRST (Thm.no_prems, size_of_thm) (step_tac ctxt 1));
 
 val _ = Theory.setup
   (Method.setup \<^binding>\<open>safe\<close> (method safe_tac) "" #>