src/ZF/intr_elim.ML
changeset 909 5de21942d046
parent 726 d703d1a1a2af
child 1418 f5f97ee67cbb
--- 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 =