src/HOL/Tools/datatype_codegen.ML
changeset 18334 a41ce9c10b73
parent 18247 b17724cae935
child 18379 87cb7e641ba5
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 02 16:04:48 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 02 16:05:12 2005 +0100
     1.3 @@ -305,19 +305,16 @@
     1.4    |> is_some;
     1.5  
     1.6  fun get_datatype thy dtname =
     1.7 -  case CodegenPackage.tname_of_idf thy dtname
     1.8 -   of SOME dtname =>
     1.9 -        dtname
    1.10 -        |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.11 -        |> Option.map #descr
    1.12 -        |> these
    1.13 -        |> get_first (fn (_, (dtname', vs, cs)) =>
    1.14 -             if dtname = dtname'
    1.15 -             then SOME (vs, map fst cs)
    1.16 -             else NONE)
    1.17 -        |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)))
    1.18 -    | _ => NONE;
    1.19 -
    1.20 +  dtname
    1.21 +  |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.22 +  |> Option.map #descr
    1.23 +  |> these
    1.24 +  |> get_first (fn (_, (dtname', vs, cs)) =>
    1.25 +       if dtname = dtname'
    1.26 +       then SOME (vs, map fst cs)
    1.27 +       else NONE)
    1.28 +  |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)));
    1.29 +  
    1.30  fun get_datacons thy (c, dtname) =
    1.31    let
    1.32      val descr =
    1.33 @@ -358,11 +355,13 @@
    1.34    CodegenPackage.set_is_datatype
    1.35      is_datatype,
    1.36    CodegenPackage.add_defgen
    1.37 -    ("datatype", CodegenPackage.defgen_datatype get_datatype),
    1.38 +    ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons),
    1.39    CodegenPackage.add_defgen
    1.40      ("datacons", CodegenPackage.defgen_datacons get_datacons),
    1.41 -  CodegenPackage.add_codegen_expr
    1.42 -    ("case", CodegenPackage.codegen_case get_case_const_data)
    1.43 +  CodegenPackage.add_defgen
    1.44 +    ("dataeq", CodegenPackage.defgen_datatype_eqinst get_datatype),
    1.45 +  CodegenPackage.add_appgen
    1.46 +    ("case", CodegenPackage.appgen_case get_case_const_data)
    1.47  ];
    1.48  
    1.49  end;