src/HOL/Tools/Quotient/quotient_term.ML

          if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
   | (Const (@{const_name Ex1}, ty) $ (Abs (_, _,
-      (Const (@{const_name "op &"}, _) $ (Const (@{const_name Set.member}, _) $ _ $
+      (Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $
         (Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))),
      Const (@{const_name Ex1}, ty') $ t') =>
        let
          val t_ = incr_boundvars (~1) t
          val subtrm = apply_subt (regularize_trm ctxt) (t_, t')