src/ZF/pair.ML

   [ (rtac (major RS equalityD1 RS subsetD RS emptyE) 1),
     (rtac consI1 1) ]);
 
 val Pair_neq_fst = prove_goalw ZF.thy [Pair_def] "<a,b>=a ==> P"
  (fn [major]=>
-  [ (rtac (consI1 RS mem_anti_sym RS FalseE) 1),
+  [ (rtac (consI1 RS mem_asym RS FalseE) 1),
     (rtac (major RS subst) 1),
     (rtac consI1 1) ]);
 
 val Pair_neq_snd = prove_goalw ZF.thy [Pair_def] "<a,b>=b ==> P"
  (fn [major]=>
-  [ (rtac (consI1 RS consI2 RS mem_anti_sym RS FalseE) 1),
+  [ (rtac (consI1 RS consI2 RS mem_asym RS FalseE) 1),
     (rtac (major RS subst) 1),
     (rtac (consI1 RS consI2) 1) ]);
 
 
 (*** Sigma: Disjoint union of a family of sets