# HG changeset patch
# User berghofe
# Date 1106586569 -3600
# Node ID 16dd63c7804931a0578c34a8dea40f0c7e9c05f1
# Parent  9c292e3e0ca11f4b823ce8f38798395ef720121f
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.

diff -r 9c292e3e0ca1 -r 16dd63c78049 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Jan 24 18:07:10 2005 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Jan 24 18:09:29 2005 +0100
@@ -108,21 +108,7 @@
         (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
           (1 upto (length descr'))));
 
-    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
-      replicate (length descr') HOLogic.typeS);
-
-    val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
-      map (fn (_, cargs) =>
-        let
-          val Ts = map (typ_of_dtyp descr' sorts) cargs;
-          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
-
-          fun mk_argT (dt, T) =
-            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
-
-          val argTs = Ts @ map mk_argT recs
-        in argTs ---> nth_elem (i, rec_result_Ts)
-        end) constrs) descr');
+    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
 
     val rec_set_Ts = map (fn (T1, T2) => reccomb_fn_Ts ---> HOLogic.mk_setT
       (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
diff -r 9c292e3e0ca1 -r 16dd63c78049 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Mon Jan 24 18:07:10 2005 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Mon Jan 24 18:09:29 2005 +0100
@@ -13,6 +13,8 @@
   val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
   val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
   val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
+  val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
+    string list -> typ list * typ list
   val make_primrecs : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> term list
   val make_cases : string list -> DatatypeAux.descr list ->
@@ -152,13 +154,9 @@
 
 (*************** characteristic equations for primrec combinator **************)
 
-fun make_primrecs new_type_names descr sorts thy =
+fun make_primrec_Ts descr sorts used =
   let
-    val sign = Theory.sign_of thy;
-
     val descr' = flat descr;
-    val recTs = get_rec_types descr' sorts;
-    val used = foldr add_typ_tfree_names (recTs, []);
 
     val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
       replicate (length descr') HOLogic.typeS);
@@ -176,6 +174,18 @@
         in argTs ---> nth_elem (i, rec_result_Ts)
         end) constrs) descr');
 
+  in (rec_result_Ts, reccomb_fn_Ts) end;
+
+fun make_primrecs new_type_names descr sorts thy =
+  let
+    val sign = Theory.sign_of thy;
+
+    val descr' = flat descr;
+    val recTs = get_rec_types descr' sorts;
+    val used = foldr add_typ_tfree_names (recTs, []);
+
+    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
+
     val rec_fns = map (uncurry (mk_Free "f"))
       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));