diff -r 807b249f1061 -r 0b3700d31758 src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/ZF/Datatype.thy	Thu Oct 19 17:06:39 2023 +0200
@@ -63,7 +63,7 @@
 structure Data_Free:
 sig
   val trace: bool Config.T
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
 end =
 struct