src/HOL/Tools/monomorph.ML
changeset 43225 142b58087974
parent 43117 5de84843685f
child 43230 dabf6e311213
child 43232 bd4d26327633
equal deleted inserted replaced
43224:97906dfd39b7 43225:142b58087974
    33   val all_schematic_consts_of: term -> typ list Symtab.table
    33   val all_schematic_consts_of: term -> typ list Symtab.table
    34   val add_schematic_consts_of: term -> typ list Symtab.table ->
    34   val add_schematic_consts_of: term -> typ list Symtab.table ->
    35     typ list Symtab.table
    35     typ list Symtab.table
    36 
    36 
    37   (* configuration options *)
    37   (* configuration options *)
       
    38   val verbose: bool Config.T
    38   val max_rounds: int Config.T
    39   val max_rounds: int Config.T
    39   val max_new_instances: int Config.T
    40   val max_new_instances: int Config.T
    40   val complete_instances: bool Config.T
    41   val complete_instances: bool Config.T
    41 
    42 
    42   (* monomorphization *)
    43   (* monomorphization *)
    61 
    62 
    62 
    63 
    63 
    64 
    64 (* configuration options *)
    65 (* configuration options *)
    65 
    66 
       
    67 val verbose = Attrib.setup_config_bool @{binding monomorph_verbose} (K true)
    66 val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
    68 val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
    67 val max_new_instances =
    69 val max_new_instances =
    68   Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
    70   Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
    69 val complete_instances =
    71 val complete_instances =
    70   Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)
    72   Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)