1.1 --- a/src/Pure/Isar/named_target.ML	Mon Apr 02 20:12:17 2012 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Mon Apr 02 20:50:41 2012 +0200
     1.3 @@ -46,11 +46,38 @@
     1.4  
     1.5  (* consts in locale *)
     1.6  
     1.7 -fun generic_const same_shape prmode ((b, mx), t) =
     1.8 -  Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
     1.9 -  #-> (fn (const as Const (c, _), _) => same_shape ?
    1.10 -        (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
    1.11 -          Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])));
    1.12 +fun generic_const same_shape prmode ((b, mx), t) context =
    1.13 +  let
    1.14 +    val const_alias =
    1.15 +      if same_shape then
    1.16 +        (case t of
    1.17 +          Const (c, T) =>
    1.18 +            let
    1.19 +              val thy = Context.theory_of context;
    1.20 +              val ctxt = Context.proof_of context;
    1.21 +              val t' = Syntax.check_term ctxt (Const (c, dummyT))
    1.22 +                |> singleton (Variable.polymorphic ctxt);
    1.23 +            in
    1.24 +              (case t' of
    1.25 +                Const (c', T') =>
    1.26 +                  if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
    1.27 +              | _ => NONE)
    1.28 +            end
    1.29 +        | _ => NONE)
    1.30 +      else NONE;
    1.31 +  in
    1.32 +    (case const_alias of
    1.33 +      SOME c =>
    1.34 +        context
    1.35 +        |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
    1.36 +        |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
    1.37 +    | NONE =>
    1.38 +        context
    1.39 +        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
    1.40 +        |-> (fn (const as Const (c, _), _) => same_shape ?
    1.41 +              (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
    1.42 +               Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
    1.43 +  end;
    1.44  
    1.45  fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
    1.46    Generic_Target.locale_declaration target true (fn phi =>