--- 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