# HG changeset patch
# User wenzelm
# Date 1482062833 -3600
# Node ID 51f8e259de50d8d2f30bba9fc3a2a3e5d7ab9c57
# Parent  511b30aa410018e47e4c378244a0be6fe43fda77
tuned messages -- more symbols;

diff -r 511b30aa4100 -r 51f8e259de50 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/Isar/overloading.ML	Sun Dec 18 13:07:13 2016 +0100
@@ -139,7 +139,7 @@
       | 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,
@@ -168,7 +168,7 @@
     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
diff -r 511b30aa4100 -r 51f8e259de50 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sun Dec 18 13:07:13 2016 +0100
@@ -95,7 +95,7 @@
     val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
 
     fun pretty_abbrev (c, (ty, t)) = Pretty.block
-      (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
+      (prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
 
     fun pretty_axm (a, t) =
       Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
diff -r 511b30aa4100 -r 51f8e259de50 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sun Dec 18 12:34:31 2016 +0100
+++ b/src/Pure/primitive_defs.ML	Sun Dec 18 13:07:13 2016 +0100
@@ -34,7 +34,7 @@
       commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
     val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
 
-    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
+    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
     val lhs = Envir.beta_eta_contract raw_lhs;
     val (head, args) = Term.strip_comb lhs;
     val head_tfrees = Term.add_tfrees head [];