src/HOL/HOLCF/Tools/cont_proc.ML
changeset 78800 0b3700d31758
parent 78793 2cb027b95188
--- a/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Oct 19 16:31:17 2023 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Thu Oct 19 17:06:39 2023 +0200
@@ -8,7 +8,7 @@
   val cont_thms: term -> thm list
   val all_cont_thms: term -> thm list
   val cont_tac: Proof.context -> int -> tactic
-  val cont_proc: Proof.context -> cterm -> thm option
+  val cont_proc: Simplifier.proc
 end
 
 structure ContProc : CONT_PROC =