diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -81,7 +81,7 @@
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
    if term_of x aconv y then
    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
 | _ => Nox)