diff -r 30bdc59198ff -r 4c10e8532d43 src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Wed Dec 14 17:24:23 1994 +0100
+++ b/src/ZF/QPair.ML	Thu Dec 15 11:08:22 1994 +0100
@@ -125,7 +125,7 @@
 val qconverse_cs = qpair_cs addSIs [qconverseI] 
 			    addSEs [qconverseD,qconverseE];
 
-qed_goal "qconverse_of_qconverse" QPair.thy
+qed_goal "qconverse_qconverse" QPair.thy
     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
 
@@ -133,7 +133,7 @@
     "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
  (fn _ => [ (fast_tac qconverse_cs 1) ]);
 
-qed_goal "qconverse_of_prod" QPair.thy "qconverse(A <*> B) = B <*> A"
+qed_goal "qconverse_prod" QPair.thy "qconverse(A <*> B) = B <*> A"
  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
 
 qed_goal "qconverse_empty" QPair.thy "qconverse(0) = 0"