src/HOL/Tools/datatype_package.ML

   val prep_ext = I;
   val merge: T * T -> T = Symtab.merge (K true);
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
 end;
 
 structure DatatypesData = TheoryDataFun(DatatypesArgs);
 val get_datatypes_sg = DatatypesData.get_sg;
 val get_datatypes = DatatypesData.get;