--- 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) "" #>