--- a/src/HOL/ex/Simult.ML Thu Sep 12 10:36:51 1996 +0200
+++ b/src/HOL/ex/Simult.ML Thu Sep 12 10:40:05 1996 +0200
@@ -64,7 +64,7 @@
AddSIs [PartI];
AddSDs [In0_inject, In1_inject];
-AddSEs [In0_neq_In1, In1_neq_In0, PartE];
+AddSEs [PartE];
(*Could prove ~ TCONS M N : Part (TF A) In1 etc. *)