44 {target = target, is_locale = is_locale, is_class = is_class}); |
44 {target = target, is_locale = is_locale, is_class = is_class}); |
45 |
45 |
46 |
46 |
47 (* consts in locale *) |
47 (* consts in locale *) |
48 |
48 |
49 fun generic_const same_shape prmode ((b, mx), t) = |
49 fun generic_const same_shape prmode ((b, mx), t) context = |
50 Proof_Context.generic_add_abbrev Print_Mode.internal (b, t) |
50 let |
51 #-> (fn (const as Const (c, _), _) => same_shape ? |
51 val const_alias = |
52 (Proof_Context.generic_revert_abbrev (#1 prmode) c #> |
52 if same_shape then |
53 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))); |
53 (case t of |
|
54 Const (c, T) => |
|
55 let |
|
56 val thy = Context.theory_of context; |
|
57 val ctxt = Context.proof_of context; |
|
58 val t' = Syntax.check_term ctxt (Const (c, dummyT)) |
|
59 |> singleton (Variable.polymorphic ctxt); |
|
60 in |
|
61 (case t' of |
|
62 Const (c', T') => |
|
63 if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE |
|
64 | _ => NONE) |
|
65 end |
|
66 | _ => NONE) |
|
67 else NONE; |
|
68 in |
|
69 (case const_alias of |
|
70 SOME c => |
|
71 context |
|
72 |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) |
|
73 |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) |
|
74 | NONE => |
|
75 context |
|
76 |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t) |
|
77 |-> (fn (const as Const (c, _), _) => same_shape ? |
|
78 (Proof_Context.generic_revert_abbrev (#1 prmode) c #> |
|
79 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) |
|
80 end; |
54 |
81 |
55 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = |
82 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = |
56 Generic_Target.locale_declaration target true (fn phi => |
83 Generic_Target.locale_declaration target true (fn phi => |
57 let |
84 let |
58 val b' = Morphism.binding phi b; |
85 val b' = Morphism.binding phi b; |