--- a/src/Pure/tctical.ML Wed Jan 03 11:14:48 2001 +0100
+++ b/src/Pure/tctical.ML Wed Jan 03 21:18:31 2001 +0100
@@ -374,7 +374,7 @@
val prop_equals = cterm_of (Theory.sign_of ProtoPure.thy)
(Const("==", propT-->propT-->propT));
-fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
+fun mk_prop_equals(t,u) = Thm.capply (Thm.capply prop_equals t) u;
(*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible.
It is paired with a function to undo the transformation. If ct contains