# HG changeset patch
# User lcp
# Date 785440083 -3600
# Node ID 711e4eb8c21358a92e73ba5e04f82c11519767a4
# Parent  d703d1a1a2af133395033277b2d6ffc390d1b57f
ZF INDUCTIVE DEFINITIONS: Simplifying the type checking for mutually
recursive datatypes, especially with monotone operators

ZF/add_ind_def/add_fp_def: deleted as obsolete

ZF/add_ind_def/add_fp_def_i: now takes dom_sum instead of domts.  We no
longer automatically construct a sum of separate domains, but could use a
sum-closed set such as univ(A).

diff -r d703d1a1a2af -r 711e4eb8c213 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Mon Nov 21 15:53:02 1994 +0100
+++ b/src/ZF/add_ind_def.ML	Mon Nov 21 18:48:03 1994 +0100
@@ -64,8 +64,7 @@
 
 signature ADD_INDUCTIVE_DEF =
   sig 
-  val add_fp_def_i : term list * term list * term list -> theory -> theory
-  val add_fp_def   : (string*string) list * string list -> theory -> theory
+  val add_fp_def_i : term list * term * term list -> theory -> theory
   val add_constructs_def :
         string list * ((string*typ*mixfix) * 
                        string * term list * term list) list list ->
@@ -81,7 +80,7 @@
 open Logic Ind_Syntax;
 
 (*internal version*)
-fun add_fp_def_i (rec_tms, domts, intr_tms) thy = 
+fun add_fp_def_i (rec_tms, dom_sum, intr_tms) thy = 
   let
     val sign = sign_of thy;
 
@@ -128,8 +127,6 @@
 	  val zeq = eq_const $ (Free(z',iT)) $ (#1 (rule_concl intr))
       in foldr mk_exists (exfrees, fold_bal (app conj) (zeq::prems)) end;
 
-    val dom_sum = fold_bal (app Su.sum) domts;
-
     (*The Part(A,h) terms -- compose injections to make h*)
     fun mk_Part (Bound 0) = Free(X',iT)	(*no mutual rec, no Part needed*)
       | mk_Part h         = Part_const $ Free(X',iT) $ Abs(w',iT,h);
@@ -174,15 +171,6 @@
   in  thy |> add_defs_i axpairs  end
 
 
-(*external, string-based version; needed?*)
-fun add_fp_def (rec_doms, sintrs) thy = 
-  let val sign = sign_of thy;
-      val rec_tms = map (readtm sign iT o fst) rec_doms
-      and domts   = map (readtm sign iT o snd) rec_doms
-      val intr_tms = map (readtm sign propT) sintrs
-  in  add_fp_def_i (rec_tms, domts, intr_tms) thy  end
-
-
 (*Expects the recursive sets to have been defined already.
   con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
 fun add_constructs_def (rec_names, con_ty_lists) thy =