src/HOL/Tools/datatype_prop.ML
changeset 15459 16dd63c78049
parent 14981 e73f8140af78
child 15531 08c8dad8e399
--- 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)));