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