# HG changeset patch
# User lcp
# Date 799515036 -7200
# Node ID 141f73abbafc7dc51ebec153b05555804927219d
# Parent  08fda51489713491007b79dd3ca56a7db52b2516
Changed to use split instead of fsplit.  The weakening of fsplitE appears not
to affect existing proofs.

diff -r 08fda5148971 -r 141f73abbafc src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Wed May 03 17:22:18 1995 +0200
+++ b/src/ZF/indrule.ML	Wed May 03 17:30:36 1995 +0200
@@ -189,7 +189,7 @@
 val fsplit_tac =
     REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, 
 			      dtac Pr.fsplitD,
-			      etac Pr.fsplitE,
+			      etac Pr.fsplitE,	(*apparently never used!*)
 			      bound_hyp_subst_tac]))
     THEN prune_params_tac;