# HG changeset patch
# User paulson
# Date 831571161 -7200
# Node ID 5a4f382455ce5835de3f3439f9f58220bc61152f
# Parent  fe0b459273f29f09833c33138c0bc0c7b03893b9
Modified to use new functor signatures

diff -r fe0b459273f2 -r 5a4f382455ce src/ZF/Inductive.ML
--- a/src/ZF/Inductive.ML	Wed May 08 17:57:05 1996 +0200
+++ b/src/ZF/Inductive.ML	Wed May 08 17:59:21 1996 +0200
@@ -29,8 +29,7 @@
   struct
   val sigma     = Const("Sigma", [iT, iT-->iT]--->iT)
   val pair      = Const("Pair", [iT,iT]--->iT)
-  val split_const       = Const("split", [[iT,iT]--->iT, iT]--->iT)
-  val fsplit_const      = Const("split", [[iT,iT]--->oT, iT]--->oT)
+  val split_name = "split"
   val pair_iff  = Pair_iff
   val split_eq  = split
   val fsplitI   = splitI
@@ -38,6 +37,8 @@
   val fsplitE   = splitE
   end;
 
+structure Standard_CP = CartProd_Fun (Standard_Prod);
+
 structure Standard_Sum =
   struct
   val sum       = Const("op +", [iT,iT]--->iT)
@@ -64,8 +65,9 @@
 
   structure Indrule = 
       Indrule_Fun (structure Inductive=Inductive and 
-                   Pr=Standard_Prod and Su=Standard_Sum and 
-                       Intr_elim=Intr_elim)
+                   Pr=Standard_Prod and CP=Standard_CP and
+                   Su=Standard_Sum and 
+                   Intr_elim=Intr_elim)
 in 
    struct 
    val thy      = Intr_elim.thy
@@ -81,7 +83,8 @@
 
 
 structure Ind = Add_inductive_def_Fun
-    (structure Fp=Lfp and Pr=Standard_Prod and Su=Standard_Sum);
+    (structure Fp=Lfp and Pr=Standard_Prod and CP=Standard_CP
+     and Su=Standard_Sum);
 
 
 structure Gfp =
@@ -98,8 +101,7 @@
   struct
   val sigma     = Const("QSigma", [iT, iT-->iT]--->iT)
   val pair      = Const("QPair", [iT,iT]--->iT)
-  val split_const       = Const("qsplit", [[iT,iT]--->iT, iT]--->iT)
-  val fsplit_const      = Const("qsplit", [[iT,iT]--->oT, iT]--->oT)
+  val split_name = "qsplit"
   val pair_iff  = QPair_iff
   val split_eq  = qsplit
   val fsplitI   = qsplitI
@@ -107,6 +109,8 @@
   val fsplitE   = qsplitE
   end;
 
+structure Quine_CP = CartProd_Fun (Quine_Prod);
+
 structure Quine_Sum =
   struct
   val sum       = Const("op <+>", [iT,iT]--->iT)
@@ -136,7 +140,8 @@
 let
   structure Intr_elim = 
       Intr_elim_Fun(structure Inductive=Inductive and Fp=Gfp and 
-                    Pr=Quine_Prod and Su=Quine_Sum);
+                    Pr=Quine_Prod and CP=Standard_CP and
+                    Su=Quine_Sum);
 in
    struct
    val thy      = Intr_elim.thy
@@ -151,5 +156,6 @@
 end;
 
 structure CoInd = 
-    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and Su=Quine_Sum);
+    Add_inductive_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
+                          and Su=Quine_Sum);