# HG changeset patch
# User wenzelm
# Date 1634124069 -7200
# Node ID 21a20b9907243a3f1ce9d4e7fbb1613c06542609
# Parent  f24ade4ff3cc55a993dd4f4caa0bf35e6e91c67e
clarified signature;

diff -r f24ade4ff3cc -r 21a20b990724 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Oct 13 13:19:09 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Oct 13 13:21:09 2021 +0200
@@ -72,7 +72,7 @@
       seconds (the secs)
   end
 
-val subgoal_count = Try.subgoal_count
+val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
 
 exception TOO_MANY of unit
 
diff -r f24ade4ff3cc -r 21a20b990724 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Oct 13 13:19:09 2021 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Oct 13 13:21:09 2021 +0200
@@ -40,6 +40,7 @@
   val refine_singleton: Method.text -> state -> state
   val refine_insert: thm list -> state -> state
   val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
+  val goal_finished: state -> bool
   val raw_goal: state -> {context: context, facts: thm list, goal: thm}
   val goal: state -> {context: context, facts: thm list, goal: thm}
   val simple_goal: state -> {context: context, goal: thm}
@@ -532,6 +533,8 @@
 
 (* goal views -- corresponding to methods *)
 
+val goal_finished = Thm.no_prems o #goal o #2 o find_goal;
+
 fun raw_goal state =
   let val (ctxt, (using, goal)) = get_goal state
   in {context = ctxt, facts = using, goal = goal} end;
diff -r f24ade4ff3cc -r 21a20b990724 src/Tools/try.ML
--- a/src/Tools/try.ML	Wed Oct 13 13:19:09 2021 +0200
+++ b/src/Tools/try.ML	Wed Oct 13 13:21:09 2021 +0200
@@ -8,7 +8,6 @@
 signature TRY =
 sig
   val serial_commas: string -> string list -> string list
-  val subgoal_count: Proof.state -> int
   type body = bool -> Proof.state -> bool * (string * string list)
   type tool = {name: string, weight: int, auto_option: string, body: body}
   val get_tools: theory -> tool list
@@ -27,8 +26,6 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss;
 
-val subgoal_count = Logic.count_prems o Thm.prop_of o #goal o Proof.goal;
-
 
 (* configuration *)
 
@@ -54,7 +51,7 @@
 (* try command *)
 
 fun try_tools state =
-  if subgoal_count state = 0 then
+  if Proof.goal_finished state then
     (writeln "No subgoal!"; NONE)
   else
     get_tools (Proof.theory_of state)