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/Pure/search.ML
changeset 81954 6f2bcdfa9a19
parent 62919 9eb0359d6a77 
--- a/src/Pure/search.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/Pure/search.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -129,7 +129,7 @@
                 let
                   val np' = Thm.nprems_of st;
                   (*rgd' calculation assumes tactic operates on subgoal 1*)
-                  val rgd' = not (has_vars (hd (Thm.prems_of st)));
+                  val rgd' = not (has_vars (hd (Thm.take_prems_of 1 st)));
                   val k' = k + np' - np + 1;  (*difference in # of subgoals, +1*)
                 in
                   if k' + np' >= bnd then depth (bnd, Int.min (inc, k' + np' + 1 - bnd)) qs
isabelle