--- a/src/HOL/List.thy Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/List.thy Thu Oct 19 21:38:09 2023 +0200
@@ -557,7 +557,7 @@
signature LIST_TO_SET_COMPREHENSION =
sig
- val simproc : Simplifier.proc
+ val proc: Simplifier.proc
end
structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =
@@ -717,7 +717,7 @@
in
-fun simproc ctxt redex =
+fun proc ctxt redex =
let
fun make_inner_eqs bound_vs Tis eqs t =
(case dest_case ctxt t of
@@ -774,7 +774,7 @@
\<close>
simproc_setup list_to_set_comprehension ("set xs") =
- \<open>K List_to_Set_Comprehension.simproc\<close>
+ \<open>K List_to_Set_Comprehension.proc\<close>
code_datatype set coset
hide_const (open) coset