src/HOL/Decision_Procs/ferrante_rackoff_data.ML

   val del: attribute
   val add: entry -> attribute 
   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;
 
 structure Ferrante_Rackoff_Data: FERRANTE_RACKOF_DATA = 
 struct