src/HOL/Tools/datatype_abs_proofs.ML
changeset 15459 16dd63c78049
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Jan 24 18:07:10 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Jan 24 18:09:29 2005 +0100
     1.3 @@ -108,21 +108,7 @@
     1.4          (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
     1.5            (1 upto (length descr'))));
     1.6  
     1.7 -    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
     1.8 -      replicate (length descr') HOLogic.typeS);
     1.9 -
    1.10 -    val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
    1.11 -      map (fn (_, cargs) =>
    1.12 -        let
    1.13 -          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.14 -          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    1.15 -
    1.16 -          fun mk_argT (dt, T) =
    1.17 -            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
    1.18 -
    1.19 -          val argTs = Ts @ map mk_argT recs
    1.20 -        in argTs ---> nth_elem (i, rec_result_Ts)
    1.21 -        end) constrs) descr');
    1.22 +    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
    1.23  
    1.24      val rec_set_Ts = map (fn (T1, T2) => reccomb_fn_Ts ---> HOLogic.mk_setT
    1.25        (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);