src/ZF/Datatype.thy

 (* Simproc for freeness reasoning: compare datatype constructors for equality *)
 
 structure Data_Free:
 sig
   val trace: bool Config.T
-  val proc: Proof.context -> cterm -> thm option
+  val proc: Simplifier.proc
 end =
 struct
 
 val trace = Attrib.setup_config_bool \<^binding>\<open>data_free_trace\<close> (K false);