Refine the supression of abbreviations for morphisms that are not identities.

--- a/NEWS	Wed Nov 18 17:37:00 2015 +0000
+++ b/NEWS	Wed Nov 18 21:18:33 2015 +0100
@@ -314,6 +314,28 @@
 * Keyword 'rewrites' identifies rewrite morphisms in interpretation
 commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
 
+* More gentle suppression of syntax along locale morphisms while
+printing terms.  Previously 'abbreviation' and 'notation' declarations
+would be suppressed for morphisms except term identity.  Now
+'abbreviation' is also kept for morphims that only change the involved
+parameters, and only 'notation' is suppressed.  This can be of great
+help when working with complex locale hierarchies, because proof
+states are displayed much more succinctly.  It also means that only
+notation needs to be redeclared if desired, as illustrated by this
+example:
+
+  locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
+  begin
+    definition derived (infixl "\<odot>" 65) where ...
+  end
+
+  locale morphism =
+    left: struct composition + right: struct composition'
+    for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
+  begin
+    notation right.derived ("\<odot>''")
+  end
+
 * Command 'sublocale' accepts mixin definitions after keyword
 'defines'.
 

--- a/src/Doc/Locales/Examples1.thy	Wed Nov 18 17:37:00 2015 +0000
+++ b/src/Doc/Locales/Examples1.thy	Wed Nov 18 21:18:33 2015 +0100
@@ -70,13 +70,13 @@
   The prefix @{text int} is applied to all names introduced in locale
   conclusions including names introduced in definitions.  The
   qualified name @{text int.less} is short for
-  the interpretation of the definition, which is @{term int.less}.
+  the interpretation of the definition, which is @{text "partial_order.less op \<le>"}.
   Qualified name and expanded form may be used almost
   interchangeably.%
-\footnote{Since @{term "op \<le>"} is polymorphic, for @{term int.less} a
+\footnote{Since @{term "op \<le>"} is polymorphic, for @{text "partial_order.less op \<le>"} a
   more general type will be inferred than for @{text int.less} which
   is over type @{typ int}.}
-  The latter is preferred on output, as for example in the theorem
+  The former is preferred on output, as for example in the theorem
   @{thm [source] int.less_le_trans}: @{thm [display, indent=2]
   int.less_le_trans}
   Both notations for the strict order are not satisfactory.  The

--- a/src/Doc/Locales/Examples3.thy	Wed Nov 18 17:37:00 2015 +0000
+++ b/src/Doc/Locales/Examples3.thy	Wed Nov 18 21:18:33 2015 +0100
@@ -223,15 +223,13 @@
 
   \hspace*{1em}@{thm [source] le'.less_le_trans}:
   @{thm [display, indent=4] le'.less_le_trans}
-  While there is infix syntax for the strict operation associated to
+  While there is infix syntax for the strict operation associated with
   @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
-  "op \<preceq>"}.  The abbreviation @{text less} with its infix syntax is only
+  "op \<preceq>"}.  The syntax @{text "\<sqsubset>"} for @{text less} is only
   available for the original instance it was declared for.  We may
-  introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>}
-  with the following declaration:\<close>
+  introduce infix syntax for @{text le'.less} with the following declaration:\<close>
 
-  abbreviation (in order_preserving)
-    less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
+  notation (in order_preserving) le'.less (infixl "\<prec>" 50)
 
 text (in order_preserving) \<open>Now the theorem is displayed nicely as
   @{thm [source]  le'.less_le_trans}:
@@ -306,8 +304,8 @@
 
   context lattice_hom
   begin
-  abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
-  abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
+  notation le'.meet (infixl "\<sqinter>''" 50)
+  notation le'.join (infixl "\<squnion>''" 50)
   end
 
 text \<open>The next example makes radical use of the short hand

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 18 17:37:00 2015 +0000
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 18 21:18:33 2015 +0100
@@ -126,26 +126,7 @@
 thm var.test_def
 
 
-text \<open>Under which circumstances term syntax remains active.\<close>
-
-locale "syntax" =
-  fixes p1 :: "'a => 'b"
-    and p2 :: "'b => o"
-begin
-
-definition d1 :: "'a => o" where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
-definition d2 :: "'b => o" where "d2(x) \<longleftrightarrow> \<not> p2(x)"
-
-thm d1_def d2_def
-
-end
-
-thm syntax.d1_def syntax.d2_def
-
-locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
-begin
-
-thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
+text \<open>Under which circumstances notation remains active.\<close>
 
 ML \<open>
   fun check_syntax ctxt thm expected =
@@ -161,9 +142,28 @@
 
 declare [[show_hyps]]
 
+locale "syntax" =
+  fixes p1 :: "'a => 'b"
+    and p2 :: "'b => o"
+begin
+
+definition d1 :: "'a => o" ("D1'(_')") where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
+definition d2 :: "'b => o" ("D2'(_')") where "d2(x) \<longleftrightarrow> \<not> p2(x)"
+
+thm d1_def d2_def
+
+end
+
+thm syntax.d1_def syntax.d2_def
+
+locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
+begin
+
+thm d1_def d2_def  (* should print as "D1(?x) <-> ..." and "D2(?x) <-> ..." *)
+
 ML \<open>
-  check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
-  check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
+  check_syntax @{context} @{thm d1_def} "D1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
+  check_syntax @{context} @{thm d2_def} "D2(?x) \<longleftrightarrow> \<not> p2(?x)";
 \<close>
 
 end
@@ -172,11 +172,11 @@
 begin
 
 thm d1_def d2_def
-  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
+  (* should print as "d1(?x) <-> ..." and "D2(?x) <-> ..." *)
 
 ML \<open>
-  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) \<longleftrightarrow> \<not> p2(p3(?x))";
-  check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
+  check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p3(?x))";
+  check_syntax @{context} @{thm d2_def} "D2(?x) \<longleftrightarrow> \<not> p2(?x)";
 \<close>
 
 end

--- a/src/Pure/Isar/generic_target.ML	Wed Nov 18 17:37:00 2015 +0000
+++ b/src/Pure/Isar/generic_target.ML	Wed Nov 18 21:18:33 2015 +0100
@@ -112,12 +112,17 @@
   else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
     Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
 
+fun same_const (Const (c, _), Const (c', _)) = c = c'
+  | same_const (t $ _, t' $ _) = same_const (t, t')
+  | same_const (_, _) = false;
+
 fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
   if phi_pred phi then
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
       val same_shape = Term.aconv_untyped (rhs, rhs');
+      val same_stem = same_shape orelse same_const (rhs, rhs');
       val const_alias =
         if same_shape then
           (case rhs' of
@@ -141,9 +146,9 @@
       | NONE =>
           context
           |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
-          |-> (fn (const as Const (c, _), _) => same_shape ?
+          |-> (fn (const as Const (c, _), _) => same_stem ?
                 (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
-                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+                 same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
     end
   else context;