# HG changeset patch
# User lcp
# Date 793903483 -3600
# Node ID 5de21942d0466e6940f093243beb4c575aedfc2e
# Parent  1f99a44c10cbd5ccc1431c5500acca0115911d05
intro_tacsf now includes subsetI as an introduction rule.  It is
needed for rules like list_into_univ

diff -r 1f99a44c10cb -r 5de21942d046 src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Mon Feb 27 17:40:57 1995 +0100
+++ b/src/ZF/intr_elim.ML	Mon Feb 27 17:44:43 1995 +0100
@@ -110,7 +110,7 @@
    REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
 		      ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::type_elims)
 		      ORELSE' hyp_subst_tac)),
-   DEPTH_SOLVE (swap_res_tac (SigmaI::type_intrs) 1)];
+   DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)];
 
 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*)
 val mk_disj_rls =