diff -r 9ab8873bf9b3 -r 200a16083201 src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/QPair.ML	Wed Dec 14 11:41:49 1994 +0100
@@ -29,7 +29,7 @@
     "<a;b> = <c;d> <-> a=c & b=d"
  (fn _=> [rtac sum_equal_iff 1]);
 
-val QPair_inject = standard (QPair_iff RS iffD1 RS conjE);
+bind_thm ("QPair_inject", (QPair_iff RS iffD1 RS conjE));
 
 qed_goal "QPair_inject1" QPair.thy "<a;b> = <c;d> ==> a=c"
  (fn [major]=>
@@ -203,10 +203,10 @@
 
 (*Injection and freeness rules*)
 
-val QInl_inject = standard (QInl_iff RS iffD1);
-val QInr_inject = standard (QInr_iff RS iffD1);
-val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE);
-val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
+bind_thm ("QInl_inject", (QInl_iff RS iffD1));
+bind_thm ("QInr_inject", (QInr_iff RS iffD1));
+bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
+bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
 
 val qsum_cs = 
     qpair_cs addSIs [PartI, QInlI, QInrI]