Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed superfluous `op'
authornipkow
Fri, 06 Mar 1998 16:05:04 +0100
changeset 4684 eb712fef644b
parent 4683 de426efe87d3
child 4685 9259feeeb2c8
Removed superfluous `op'
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle