src/HOL/Tools/Function/partial_function.ML

 structure Modes = Generic_Data
 (
   type T = ((term * term) * thm) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  fun merge (a, b) = Symtab.merge (K true) (a, b);
+  fun merge data = Symtab.merge (K true) data;
 )
 
 fun init fixp mono fixp_eq phi =
   let
     val term = Morphism.term phi;