# HG changeset patch
# User nipkow
# Date 1755376544 -7200
# Node ID b01548bf9e77b4dd41136f6195a9be1b99b80a23
# Parent  3f3d83b9ffbc6d3298b737593c9c077149e3aabd# Parent  5ac432dba04572c269eff4235ce4b89c9884f4ed
merged

diff -r 3f3d83b9ffbc -r b01548bf9e77 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Aug 16 13:06:26 2025 +0200
+++ b/src/HOL/List.thy	Sat Aug 16 22:35:44 2025 +0200
@@ -798,11 +798,9 @@
                 val lhs = Thm.term_of redex
                 val rhs = HOLogic.mk_Collect ("x", rT, inner_t)
                 val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
-              in
-                SOME
-                  ((Goal.prove ctxt [] [] rewrite_rule_t
-                    (fn {context = ctxt', ...} => tac ctxt' (rev Tis))) RS @{thm eq_reflection})
-              end))
+                val eq_thm = Goal.norm_result ctxt (Goal.prove_internal ctxt []
+                  (Thm.cterm_of ctxt rewrite_rule_t) (fn _ => tac ctxt (rev Tis)))
+              in SOME (eq_thm RS @{thm eq_reflection}) end))
   in
     make_inner_eqs [] [] [] (dest_set (Thm.term_of redex))
   end