# HG changeset patch
# User nipkow
# Date 889196704 -3600
# Node ID eb712fef644ba5bdfbc5007eaf695ecfe42277ff
# Parent  de426efe87d3218041f641e03198d9e7bb1858fe
Removed superfluous `op'

diff -r de426efe87d3 -r eb712fef644b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Mar 06 15:58:16 1998 +0100
+++ b/src/Pure/thm.ML	Fri Mar 06 16:05:04 1998 +0100
@@ -1603,7 +1603,7 @@
   orelse
    is_Var (head_of lhs)
   orelse
-   (exists (apl (lhs, op Logic.occs)) (rhs :: prems))
+   (exists (apl (lhs, Logic.occs)) (rhs :: prems))
   orelse
    (null prems andalso
     Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))