src/ZF/intr_elim.ML

--- a/src/ZF/intr_elim.ML	Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/intr_elim.ML	Thu Sep 26 15:14:23 1996 +0200
@@ -98,7 +98,7 @@
 fun intro_tacsf disjIn prems = 
   [(*insert prems and underlying sets*)
    cut_facts_tac prems 1,
-   DETERM (rtac (unfold RS ssubst) 1),
+   DETERM (stac unfold 1),
    REPEAT (resolve_tac [Part_eqI,CollectI] 1),
    (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
    rtac disjIn 2,