diff -r 053c69cb4a0e -r 4abe644fcea5 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/inductive_set.ML	Sat Aug 28 16:14:32 2010 +0200
@@ -265,7 +265,7 @@
 
 fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
   case prop_of thm of
-    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
+    Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ lhs $ rhs) =>
       (case body_type T of
          @{typ bool} =>
            let