src/Doc/Isar_Ref/Generic.thy

--- a/src/Doc/Isar_Ref/Generic.thy	Tue May 23 20:11:15 2023 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Tue May 23 21:43:36 2023 +0200
@@ -840,9 +840,9 @@
 
 (*<*)experiment begin(*>*)
 simproc_setup unit ("x::unit") =
-  \<open>fn _ => fn _ => fn ct =>
+  \<open>K (K (fn ct =>
     if HOLogic.is_unit (Thm.term_of ct) then NONE
-    else SOME (mk_meta_eq @{thm unit_eq})\<close>
+    else SOME (mk_meta_eq @{thm unit_eq})))\<close>
 (*<*)end(*>*)
 
 text \<open>