--- 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
--- 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;
--- 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)