--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu May 18 15:34:01 2023 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Thu May 18 17:21:29 2023 +0200
@@ -15,7 +15,7 @@
val funs: thm ->
{isolate_conv: morphism -> Proof.context -> cterm list -> cterm -> thm,
whatis: morphism -> cterm -> cterm -> ord,
- simpset: morphism -> Proof.context -> simpset} -> declaration
+ simpset: morphism -> Proof.context -> simpset} -> Morphism.declaration_fn
val match: Proof.context -> cterm -> entry option
end;