src/HOL/Tools/Datatype/datatype_prop.ML

           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
         in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
-           foldr1 (HOLogic.mk_binop "op &")
+           foldr1 (HOLogic.mk_binop @{const_name "op &"})
              (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
   in
     map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
       (hd descr) (take (length (hd descr)) (get_rec_types descr' sorts))

       end;
 
     val prems = maps (fn ((i, (_, _, constrs)), T) =>
       map (make_ind_prem i T) constrs) (descr' ~~ recTs);
     val tnames = make_tnames recTs;
-    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
+    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
       (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
         (descr' ~~ recTs ~~ tnames)))
 
   in Logic.list_implies (prems, concl) end;