ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
definitions may involve ordinary pairs. (HOL/intr_elim does not require
this change)

--- a/src/ZF/intr_elim.ML	Fri Oct 21 09:53:38 1994 +0100
+++ b/src/ZF/intr_elim.ML	Fri Oct 21 09:58:05 1994 +0100
@@ -119,9 +119,12 @@
 
 (*Includes rules for succ and Pair since they are common constructions*)
 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
-		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
+		Pair_neq_0, sym RS Pair_neq_0, Pair_inject,
+		make_elim succ_inject, 
 		refl_thin, conjE, exE, disjE];
 
+(*Standard sum/products for datatypes, variant ones for codatatypes;
+  We always include Pair_inject above*)
 val sumprod_free_SEs = 
     map (gen_make_elim [conjE,FalseE])
 	([Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff]