diff -r 378ffc903bed -r 89ae86205739 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Aug 27 17:59:40 2010 +0200
@@ -679,9 +679,11 @@
 
 end;
 
-val (_, oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "cooper",
-  (fn (ctxt, t) => (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
-    (t, procedure t)))));
+val (_, oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (@{binding cooper},
+    (fn (ctxt, t) =>
+      (Thm.cterm_of (ProofContext.theory_of ctxt) o Logic.mk_equals o pairself HOLogic.mk_Trueprop)
+        (t, procedure t)))));
 
 val comp_ss = HOL_ss addsimps @{thms semiring_norm};