diff -r b0c69f4db64c -r ae8450657bf0 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 27 22:30:09 2001 +0200
+++ b/src/Pure/thm.ML	Fri Sep 28 11:04:44 2001 +0200
@@ -590,7 +590,7 @@
                 if imp=implies andalso  A aconv propA
                 then
                   Thm{sign_ref= merge_thm_sgs(thAB,thA),
-                      der = Pt.infer_derivs (curry Pt.%) der derA,
+                      der = Pt.infer_derivs (curry Pt.%%) der derA,
                       maxidx = Int.max(maxA,maxidx),
                       shyps = union_sort (shypsA, shyps),
                       hyps = union_term(hypsA,hyps),  (*dups suppressed*)
@@ -635,7 +635,7 @@
               raise THM("forall_elim: type mismatch", 0, [th])
           else let val thm = fix_shyps [th] []
                     (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
-                         der = Pt.infer_derivs' (Pt.%% o rpair (Some t)) der,
+                         der = Pt.infer_derivs' (Pt.% o rpair (Some t)) der,
                          maxidx = Int.max(maxidx, maxt),
                          shyps = [],
                          hyps = hyps,