src/Pure/Isar/overloading.ML

       (case AList.lookup (op =) overloading (c, ty) of
         SOME (v, _) => SOME (ty, Free (v, ty))
       | NONE => NONE);
     val unchecks =
       map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
-  in 
+  in
     ctxt
     |> map_improvable_syntax (K {primary_constraints = [],
       secondary_constraints = [], improve = K NONE, subst = subst,
       no_subst_in_abbrev_mode = false, unchecks = unchecks})
   end;

 fun pretty lthy =
   let
     val overloading = get_overloading lthy;
     fun pr_operation ((c, ty), (v, _)) =
       Pretty.block (Pretty.breaks
-        [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
+        [Pretty.str v, Pretty.str "\<equiv>", Proof_Context.pretty_const lthy c,
           Pretty.str "::", Syntax.pretty_typ lthy ty]);
   in
     [Pretty.block
       (Pretty.fbreaks (Pretty.keyword1 "overloading" :: map pr_operation overloading))]
   end;