src/HOL/Tools/res_axioms.ML

     in  cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf  end
     handle THM _ => [];
 
 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   Skolem functions.*)
-structure ThmCache = TheoryDataFun
+structure ThmCache = Theory_Data
 (
   type T = thm list Thmtab.table * unit Symtab.table;
   val empty = (Thmtab.empty, Symtab.empty);
-  val copy = I;
   val extend = I;
-  fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
+  fun merge ((cache1, seen1), (cache2, seen2)) : T =
     (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
 );
 
 val lookup_cache = Thmtab.lookup o #1 o ThmCache.get;
 val already_seen = Symtab.defined o #2 o ThmCache.get;