# HG changeset patch
# User lcp
# Date 799503421 -7200
# Node ID c2b3b7b7a69fd4952d8ccc4e152aca3003147155
# Parent  fdaf39a47a2b7d459346c16cbe77c707778fd55d
Changed to use split instead of fsplit.  The weakening of fsplitE appears not
to affect existing proofs.

diff -r fdaf39a47a2b -r c2b3b7b7a69f src/ZF/Inductive.ML
--- a/src/ZF/Inductive.ML	Wed May 03 14:03:19 1995 +0200
+++ b/src/ZF/Inductive.ML	Wed May 03 14:17:01 1995 +0200
@@ -29,12 +29,12 @@
   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("fsplit", [[iT,iT]--->oT, iT]--->oT)
+  val fsplit_const	= Const("split", [[iT,iT]--->oT, iT]--->oT)
   val pair_iff	= Pair_iff
   val split_eq	= split
-  val fsplitI	= fsplitI
-  val fsplitD	= fsplitD
-  val fsplitE	= fsplitE
+  val fsplitI	= splitI
+  val fsplitD	= splitD
+  val fsplitE	= splitE
   end;
 
 structure Standard_Sum =
@@ -88,12 +88,12 @@
   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("qfsplit", [[iT,iT]--->oT, iT]--->oT)
+  val fsplit_const	= Const("qsplit", [[iT,iT]--->oT, iT]--->oT)
   val pair_iff	= QPair_iff
   val split_eq	= qsplit
-  val fsplitI	= qfsplitI
-  val fsplitD	= qfsplitD
-  val fsplitE	= qfsplitE
+  val fsplitI	= qsplitI
+  val fsplitD	= qsplitD
+  val fsplitE	= qsplitE
   end;
 
 structure Quine_Sum =