# HG changeset patch
# User wenzelm
# Date 1598904305 -7200
# Node ID e5fcbf6dc687d25a015e875b2bd804d596ae7578
# Parent  6b620d91e8cc9b27ace1775c1b1d283ee122d7d9
proper use of SELECT_GOAL to confine distinct_subgoals_tac to original goal range (amending 366d39e95d3c);

diff -r 6b620d91e8cc -r e5fcbf6dc687 NEWS
--- a/NEWS	Mon Aug 31 17:18:47 2020 +0100
+++ b/NEWS	Mon Aug 31 22:05:05 2020 +0200
@@ -7,6 +7,13 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Proof method "subst" is confined to the original subgoal range: its
+included distinct_subgoals_tac no longer affects unrelated subgoals.
+Rare INCOMPATIBILITY.
+
+
 *** Isabelle/jEdit Prover IDE ***
 
 * The jEdit status line includes a widget for Isabelle/ML heap usage,
diff -r 6b620d91e8cc -r e5fcbf6dc687 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Mon Aug 31 17:18:47 2020 +0100
+++ b/src/Tools/eqsubst.ML	Mon Aug 31 22:05:05 2020 +0200
@@ -300,21 +300,17 @@
 occurrences, but all earlier ones are skipped. Thus you can use [0] to
 just find all rewrites. *)
 
-fun eqsubst_tac ctxt occs thms i st =
-  let val nprems = Thm.nprems_of st in
-    if nprems < i then Seq.empty else
+fun eqsubst_tac ctxt occs thms =
+  SELECT_GOAL
     let
       val thmseq = Seq.of_list thms;
-      fun apply_occ occ st =
+      fun apply_occ_tac occ st =
         thmseq |> Seq.maps (fn r =>
           eqsubst_tac' ctxt
             (skip_first_occs_search occ searchf_lr_unify_valid) r
-            (i + (Thm.nprems_of st - nprems)) st);
+            (Thm.nprems_of st) st);
       val sorted_occs = Library.sort (rev_order o int_ord) occs;
-    in
-      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
-    end
-  end;
+    in Seq.EVERY (map apply_occ_tac sorted_occs) #> Seq.maps distinct_subgoals_tac end;
 
 
 (* apply a substitution inside assumption j, keeps asm in the same place *)
@@ -391,22 +387,17 @@
 fun skip_first_asm_occs_search searchf sinfo occ lhs =
   skipto_skipseq occ (searchf sinfo lhs);
 
-fun eqsubst_asm_tac ctxt occs thms i st =
-  let val nprems = Thm.nprems_of st in
-    if nprems < i then Seq.empty
-    else
-      let
-        val thmseq = Seq.of_list thms;
-        fun apply_occ occ st =
-          thmseq |> Seq.maps (fn r =>
-            eqsubst_asm_tac' ctxt
-              (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
-              (i + (Thm.nprems_of st - nprems)) st);
-        val sorted_occs = Library.sort (rev_order o int_ord) occs;
-      in
-        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
-      end
-  end;
+fun eqsubst_asm_tac ctxt occs thms =
+  SELECT_GOAL
+    let
+      val thmseq = Seq.of_list thms;
+      fun apply_occ_tac occ st =
+        thmseq |> Seq.maps (fn r =>
+          eqsubst_asm_tac' ctxt
+            (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
+            (Thm.nprems_of st) st);
+      val sorted_occs = Library.sort (rev_order o int_ord) occs;
+    in Seq.EVERY (map apply_occ_tac sorted_occs) #> Seq.maps distinct_subgoals_tac end;
 
 (* combination method that takes a flag (true indicates that subst
    should be done to an assumption, false = apply to the conclusion of