src/HOL/Tools/datatype_prop.ML
changeset 15459 16dd63c78049
parent 14981 e73f8140af78
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/datatype_prop.ML	Mon Jan 24 18:07:10 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_prop.ML	Mon Jan 24 18:09:29 2005 +0100
     1.3 @@ -13,6 +13,8 @@
     1.4    val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
     1.5    val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
     1.6    val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
     1.7 +  val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
     1.8 +    string list -> typ list * typ list
     1.9    val make_primrecs : string list -> DatatypeAux.descr list ->
    1.10      (string * sort) list -> theory -> term list
    1.11    val make_cases : string list -> DatatypeAux.descr list ->
    1.12 @@ -152,13 +154,9 @@
    1.13  
    1.14  (*************** characteristic equations for primrec combinator **************)
    1.15  
    1.16 -fun make_primrecs new_type_names descr sorts thy =
    1.17 +fun make_primrec_Ts descr sorts used =
    1.18    let
    1.19 -    val sign = Theory.sign_of thy;
    1.20 -
    1.21      val descr' = flat descr;
    1.22 -    val recTs = get_rec_types descr' sorts;
    1.23 -    val used = foldr add_typ_tfree_names (recTs, []);
    1.24  
    1.25      val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
    1.26        replicate (length descr') HOLogic.typeS);
    1.27 @@ -176,6 +174,18 @@
    1.28          in argTs ---> nth_elem (i, rec_result_Ts)
    1.29          end) constrs) descr');
    1.30  
    1.31 +  in (rec_result_Ts, reccomb_fn_Ts) end;
    1.32 +
    1.33 +fun make_primrecs new_type_names descr sorts thy =
    1.34 +  let
    1.35 +    val sign = Theory.sign_of thy;
    1.36 +
    1.37 +    val descr' = flat descr;
    1.38 +    val recTs = get_rec_types descr' sorts;
    1.39 +    val used = foldr add_typ_tfree_names (recTs, []);
    1.40 +
    1.41 +    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
    1.42 +
    1.43      val rec_fns = map (uncurry (mk_Free "f"))
    1.44        (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
    1.45