# 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))