# HG changeset patch
# User nipkow
# Date 785766807 -3600
# Node ID d5c6d1fb236b2bb1823b62318ce22aed7a25d8ba
# Parent  3f5136a61a72f114495ee5a1dab7df72be4a4c4e
removed Sum-rules

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*)