theory Scratch imports Main begin (* A contrieved example *) definition "enumhd = hd Enum.enum" definition "code = ([enumhd,enumhd,enumhd,enumhd,enumhd,enumhd] :: (bool*bool*bool*bool*bool) list)" (* To inspect the code *) export_code code in SML file_prefix "enumhd" (* Result: code that contains many copies of enumhd (Enum.enum_prod Enum.enum_bool (Enum.enum_prod Enum.enum_bool (Enum.enum_prod Enum.enum_bool (Enum.enum_prod Enum.enum_bool Enum.enum_bool)))) The type classes are contructed over and over at runtime and slow down compiling. *) (* Running the code *) value code (* This should give us potential speedups *) code_reflect enumhd functions enumhd (* But it does not work because code_reflect produces ML function with different type class arguments *) value code