1(* Title: HOL/Tools/Old_Datatype/old_datatype_codegen.ML 2 Author: Stefan Berghofer and Florian Haftmann, TU Muenchen 3 4Code generator facilities for inductive datatypes. 5*) 6 7signature OLD_DATATYPE_CODEGEN = 8sig 9end; 10 11structure Old_Datatype_Codegen : OLD_DATATYPE_CODEGEN = 12struct 13 14fun add_code_for_datatype fcT_name thy = 15 let 16 val ctxt = Proof_Context.init_global thy 17 val SOME {ctrs, injects, distincts, case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt fcT_name 18 val Type (_, As) = body_type (fastype_of (hd ctrs)) 19 in 20 Ctr_Sugar_Code.add_ctr_code fcT_name As (map dest_Const ctrs) injects distincts case_thms thy 21 end; 22 23val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_code_for_datatype))); 24 25end; 26