# HG changeset patch
# User lcp
# Date 785671044 -3600
# Node ID faa3efc1d130754bcdaf897c7a42db28bcbad942
# Parent  5b0dedadb5c235a857bdc7c64254fae2ed496698
data_domain,Codata_domain: removed replicate; now return one
single domain

diff -r 5b0dedadb5c2 -r faa3efc1d130 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Thu Nov 24 10:53:46 1994 +0100
+++ b/src/ZF/ind_syntax.ML	Thu Nov 24 10:57:24 1994 +0100
@@ -117,11 +117,10 @@
        | iargs => fold_bal (app Un) iargs
   end;
 
-fun data_domain rec_tms =
-  replicate (length rec_tms) (univ $ union_params (hd rec_tms));
-
-fun Codata_domain rec_tms =
-  replicate (length rec_tms) (quniv $ union_params (hd rec_tms));
+(*Previously these both did    replicate (length rec_tms);  however now
+  [q]univ itself constitutes the sum domain for mutual recursion!*)
+fun data_domain rec_tms = univ $ union_params (hd rec_tms);
+fun Codata_domain rec_tms = quniv $ union_params (hd rec_tms);
 
 (*Could go to FOL, but it's hardly general*)
 val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"