diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -338,7 +338,7 @@
       => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
-| (Const (@{const_name "op ="},_) $
+| (Const (@{const_name HOL.eq},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
@@ -350,7 +350,7 @@
       => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
-| Const (@{const_name "op ="},_) $
+| Const (@{const_name HOL.eq},_) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
@@ -370,13 +370,13 @@
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
+| Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
    (rtac @{thm refl} ORELSE'
     (equals_rsp_tac R ctxt THEN' RANGE [
        quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
 
     (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
+| Const (@{const_name HOL.eq},_) $ _ $ _ => rtac @{thm refl}
 
    (* respectfulness of constants; in particular of a simple relation *)
 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)