# 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 "\", 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 " \", 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 (\)"; val lhs = Envir.beta_eta_contract raw_lhs; val (head, args) = Term.strip_comb lhs; val head_tfrees = Term.add_tfrees head [];