src/ZF/QPair.ML
changeset 516 1957113f0d7d
parent 55 331d93292ee0
child 744 2054fa3c8d76
--- a/src/ZF/QPair.ML	Fri Aug 12 12:28:46 1994 +0200
+++ b/src/ZF/QPair.ML	Fri Aug 12 12:51:34 1994 +0200
@@ -208,8 +208,8 @@
 val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
 
 val qsum_cs = 
-    ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
-          addSDs [QInl_inject,QInr_inject];
+    qpair_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
+             addSDs [QInl_inject,QInr_inject];
 
 goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
 by (fast_tac qsum_cs 1);