# HG changeset patch
# User wenzelm
# Date 1333390337 -7200
# Node ID daef54bad4203b3cca7e62dbc8d155bb3195a9c3
# Parent  5e96bfb4a1594aa0a1ac23c1102ee791e9c9759d
tuned;

diff -r 5e96bfb4a159 -r daef54bad420 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Apr 02 19:54:25 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Apr 02 20:12:17 2012 +0200
@@ -46,6 +46,12 @@
 
 (* consts in locale *)
 
+fun generic_const same_shape prmode ((b, mx), t) =
+  Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
+  #-> (fn (const as Const (c, _), _) => same_shape ?
+        (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
+          Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])));
+
 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
   Generic_Target.locale_declaration target true (fn phi =>
     let
@@ -61,14 +67,7 @@
           andalso not (null prefix')
           andalso List.last prefix' = (Class.class_prefix target, false)
         orelse same_shape);
-    in
-      not is_canonical_class ?
-        (Proof_Context.generic_add_abbrev Print_Mode.internal (b', rhs'')
-        #-> (fn (lhs' as Const (d, _), _) =>
-            same_shape ?
-              (Proof_Context.generic_revert_abbrev mode d #>
-               Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)]))))
-    end);
+    in not is_canonical_class ? generic_const same_shape prmode ((b', mx), rhs'') end);
 
 
 (* define *)