--- a/src/HOL/Library/refute.ML Wed Oct 13 11:04:35 2021 +0200
+++ b/src/HOL/Library/refute.ML Wed Oct 13 13:19:09 2021 +0200
@@ -1201,7 +1201,7 @@
let
val t = th |> Thm.prop_of
in
- if Logic.count_prems t = 0 then
+ if Logic.no_prems t then
(writeln "No subgoal!"; "none")
else
let