diff -r 053c69cb4a0e -r 4abe644fcea5 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -179,7 +179,7 @@
 
 fun translate_literal ctxt constant_table t =
   case strip_comb t of
-    (Const (@{const_name "op ="}, _), [l, r]) =>
+    (Const (@{const_name HOL.eq}, _), [l, r]) =>
       let
         val l' = translate_term ctxt constant_table l
         val r' = translate_term ctxt constant_table r