diff -r 3f5136a61a72 -r d5c6d1fb236b ind_syntax.ML
--- a/ind_syntax.ML	Fri Nov 25 11:10:26 1994 +0100
+++ b/ind_syntax.ML	Fri Nov 25 13:33:27 1994 +0100
@@ -136,7 +136,7 @@
 (*For simplifying the elimination rule*)
 val sumprod_free_SEs = 
     Pair_inject ::
-    map make_elim [Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject];
+    map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)];
 
 (*For deriving cases rules.  
   read_instantiate replaces a propositional variable by a formula variable*)