# HG changeset patch
# User wenzelm
# Date 1634123949 -7200
# Node ID f24ade4ff3cc55a993dd4f4caa0bf35e6e91c67e
# Parent  3315c551fe6e149ed2f926dda98021930729e45f
clarified signature;

diff -r 3315c551fe6e -r f24ade4ff3cc src/HOL/Library/refute.ML
--- 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
diff -r 3315c551fe6e -r f24ade4ff3cc src/HOL/Tools/Nunchaku/nunchaku.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku.ML	Wed Oct 13 11:04:35 2021 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku.ML	Wed Oct 13 13:19:09 2021 +0200
@@ -326,7 +326,7 @@
     val ctxt = Proof.context_of state;
     val goal = Thm.prop_of (#goal (Proof.raw_goal state));
   in
-    if Logic.count_prems goal = 0 then
+    if Logic.no_prems goal then
       (writeln "No subgoal!"; (noneN, NONE))
     else
       let
diff -r 3315c551fe6e -r f24ade4ff3cc src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Oct 13 11:04:35 2021 +0200
+++ b/src/Pure/Isar/element.ML	Wed Oct 13 13:19:09 2021 +0200
@@ -390,7 +390,7 @@
         fun decomp_simp prop =
           let
             val ctxt = Proof_Context.init_global thy;
-            val _ = Logic.count_prems prop = 0 orelse
+            val _ = Logic.no_prems prop orelse
               error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
             val lhsrhs = Logic.dest_equals prop
               handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop);
diff -r 3315c551fe6e -r f24ade4ff3cc src/Pure/logic.ML
--- a/src/Pure/logic.ML	Wed Oct 13 11:04:35 2021 +0200
+++ b/src/Pure/logic.ML	Wed Oct 13 13:19:09 2021 +0200
@@ -25,6 +25,7 @@
   val strip_imp_concl: term -> term
   val strip_prems: int * term list * term -> term list * term
   val count_prems: term -> int
+  val no_prems: 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
@@ -208,6 +209,9 @@
 fun count_prems (Const ("Pure.imp", _) $ _ $ B) = 1 + count_prems B
   | count_prems _ = 0;
 
+fun no_prems (Const ("Pure.imp", _) $ _ $ _) = false
+  | no_prems _ = true;
+
 (*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)
diff -r 3315c551fe6e -r f24ade4ff3cc src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Oct 13 11:04:35 2021 +0200
+++ b/src/Pure/raw_simplifier.ML	Wed Oct 13 13:19:09 2021 +0200
@@ -981,7 +981,7 @@
           else Thm.match (elhs', eta_t');
         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = Thm.prop_of thm';
-        val unconditional = (Logic.count_prems prop' = 0);
+        val unconditional = Logic.no_prems prop';
         val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
         val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
       in
diff -r 3315c551fe6e -r f24ade4ff3cc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Oct 13 11:04:35 2021 +0200
+++ b/src/Pure/thm.ML	Wed Oct 13 13:19:09 2021 +0200
@@ -495,7 +495,7 @@
 val concl_of = Logic.strip_imp_concl o prop_of;
 val prems_of = Logic.strip_imp_prems o prop_of;
 val nprems_of = Logic.count_prems o prop_of;
-fun no_prems th = nprems_of th = 0;
+val no_prems = Logic.no_prems o prop_of;
 
 fun major_prem_of th =
   (case prems_of th of