
diff -r 0b3700d31758 -r 42ae6e0ecfd4 src/HOL/List.thy
--- 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




