src/ZF/indrule.ML
changeset 1104 141f73abbafc
parent 751 f0aacbcedb77
child 1418 f5f97ee67cbb
--- 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;