Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 74510 21a20b990724
parent 73383 6b104dc069de
child 77825 61f652dd955a 
--- 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
isabelle