(* Author: Christian Urban data about nominal datatypes *)signature NOMINAL_DT_DATA =sig type info = {inject : thm list, distinct : thm list, strong_inducts : thm list, strong_exhaust : thm list} val get_all_info: Proof.context -> (string * info) list val get_info: Proof.context -> string -> info option val the_info: Proof.context -> string -> info val register_info: (string * info) -> Context.generic -> Context.generic val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) listendstructure Nominal_Dt_Data: NOMINAL_DT_DATA =struct(* information generated by nominal_datatype *)type info = {inject : thm list, distinct : thm list, strong_inducts : thm list, strong_exhaust : thm list}structure NominalData = Generic_Data (type T = info Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.merge (K true))val get_all_info = Symtab.dest o NominalData.get o Context.Proofval get_info = Symtab.lookup o NominalData.get o Context.Proofval register_info = NominalData.map o Symtab.updatefun the_info thy name = (case get_info thy name of SOME info => info | NONE => error ("Unknown nominal datatype " ^ quote name))fun mk_infos ty_names inject distinct strong_inducts strong_exhaust =let fun aux ty_name = (ty_name, {inject = inject, distinct = distinct, strong_inducts = strong_inducts, strong_exhaust = strong_exhaust })in map aux ty_namesendend