src/Pure/meta_simplifier.ML
changeset 16842 5979c46853d1
parent 16807 730cace0ae48
child 16861 7446b4be013b
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4    andalso not(exists_subterm is_Var lhs)
     1.5      orelse
     1.6  *)
     1.7 -  exists (apl (lhs, Logic.occs)) (rhs :: prems)
     1.8 +  exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
     1.9      orelse
    1.10    null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
    1.11      (*the condition "null prems" is necessary because conditional rewrites