# HG changeset patch
# User nipkow
# Date 1755376528 -7200
# Node ID 5ac432dba04572c269eff4235ce4b89c9884f4ed
# Parent  304519f22c2ce13b646ae8e2864ae808482f1f35
use prove_internal instead of prove in list to set simproc to avoid incomplete matching sanity check

diff -r 304519f22c2c -r 5ac432dba045 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 13 09:34:57 2025 +0200
+++ b/src/HOL/List.thy	Sat Aug 16 22:35:28 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