--- a/src/HOL/Finite_Set.thy Tue May 23 20:11:15 2023 +0200
+++ b/src/HOL/Finite_Set.thy Tue May 23 21:43:36 2023 +0200
@@ -193,7 +193,7 @@
lemma finite_subset: "A \<subseteq> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
by (rule rev_finite_subset)
-simproc_setup finite ("finite A") = \<open>fn _ =>
+simproc_setup finite ("finite A") = \<open>
let
val finite_subset = @{thm finite_subset}
val Eq_TrueI = @{thm Eq_TrueI}
@@ -209,17 +209,17 @@
fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
- fun proc ss ct =
+ fun proc ctxt ct =
(let
val _ $ A = Thm.term_of ct
- val prems = Simplifier.prems_of ss
+ val prems = Simplifier.prems_of ctxt
val fins = map_filter is_finite prems
val subsets = map_filter (is_subset A) prems
in case fold_product comb subsets fins [] of
(sub_th,fin_th) :: _ => SOME((fin_th RS (sub_th RS finite_subset)) RS Eq_TrueI)
| _ => NONE
end)
-in proc end
+in K proc end
\<close>
(* Needs to be used with care *)