diff -r 5347c9a22897 -r 5e4871c5136b src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/QPair.ML	Wed Jan 13 11:57:09 1999 +0100
@@ -122,11 +122,9 @@
 (*** Eliminator - qsplit ***)
 
 (*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "qsplit" thy [qsplit_def]
-    "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
- (fn _ => [ (Simp_tac 1),
-            (rtac reflexive_thm 1) ]);
-
+Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
+by (Simp_tac 1);
+qed "qsplit";
 Addsimps [qsplit];
 
 qed_goal "qsplit_type" thy