# HG changeset patch
# User wenzelm
# Date 1737578105 -3600
# Node ID 02d9844ff8928f4bbb3f328cc743c8b99b78f752
# Parent  4652c6b36ee8e3a604fd046371a7ff48c65a137d
tuned: prefer Thm.prem_of, which differes wrt. exceptions that are not handled here;

diff -r 4652c6b36ee8 -r 02d9844ff892 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Wed Jan 22 21:31:45 2025 +0100
+++ b/src/FOLP/simp.ML	Wed Jan 22 21:35:05 2025 +0100
@@ -83,9 +83,7 @@
           biresolve_tac ctxt (Net.unify_term net
                        (lhs_of (Logic.strip_assums_concl prem))) i);
 
-fun nth_subgoal i thm = nth (Thm.prems_of thm) (i - 1);
-
-fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
+fun goal_concl i thm = Logic.strip_assums_concl (Thm.prem_of thm i);
 
 fun lhs_of_eq i thm = lhs_of(goal_concl i thm)
 and rhs_of_eq i thm = rhs_of(goal_concl i thm);
@@ -370,7 +368,7 @@
 
 (*Select subgoal i from proof state; substitute parameters, for printing*)
 fun prepare_goal i st =
-    let val subgi = nth_subgoal i st
+    let val subgi = Thm.prem_of st i
         val params = rev (Logic.strip_params subgi)
     in variants_abs (params, Logic.strip_assums_concl subgi) end;
 
@@ -425,7 +423,7 @@
 (*NB: the "Adding rewrites:" trace will look strange because assumptions
       are represented by rules, generalized over their parameters*)
 fun add_asms(ss,thm,a,anet,ats,cs) =
-    let val As = strip_varify(nth_subgoal i thm, a, []);
+    let val As = strip_varify(Thm.prem_of thm i, a, []);
         val thms = map (Thm.trivial o Thm.cterm_of ctxt) As;
         val new_rws = maps mk_rew_rules thms;
         val rwrls = map mk_trans (maps mk_rew_rules thms);
@@ -532,7 +530,7 @@
 
 fun find_subst ctxt T =
 let fun find (thm::thms) =
-        let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm));
+        let val (Const(_,cT), va, vb) = dest_red(Thm.prem_of thm 1);
             val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, []));
             val eqT::_ = binder_types cT
         in if Sign.typ_instance (Proof_Context.theory_of ctxt) (T,eqT) then SOME(thm,va,vb,P)