src/HOL/Tools/datatype_package/datatype_realizer.ML
changeset 31737 b3f63611784e
parent 31723 f5cafe803b55
     1.1 --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML	Sun Jun 21 08:38:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Sun Jun 21 08:38:58 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature DATATYPE_REALIZER =
     1.6  sig
     1.7 -  val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
     1.8 +  val add_dt_realizers: Datatype.config -> string list -> theory -> theory
     1.9    val setup: theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -38,7 +38,7 @@
    1.13  
    1.14  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
    1.15  
    1.16 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
    1.17 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy =
    1.18    let
    1.19      val recTs = get_rec_types descr sorts;
    1.20      val pnames = if length descr = 1 then ["P"]
    1.21 @@ -157,7 +157,7 @@
    1.22    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    1.23  
    1.24  
    1.25 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
    1.26 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy =
    1.27    let
    1.28      val cert = cterm_of thy;
    1.29      val rT = TFree ("'P", HOLogic.typeS);