98 (* abbrev *) |
98 (* abbrev *) |
99 |
99 |
100 fun locale_abbrev ta prmode ((b, mx), t) xs = |
100 fun locale_abbrev ta prmode ((b, mx), t) xs = |
101 Local_Theory.background_theory_result |
101 Local_Theory.background_theory_result |
102 (Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
102 (Sign.add_abbrev Print_Mode.internal (b, t)) #-> |
103 (fn (lhs, _) => locale_const ta prmode |
103 (fn (lhs, _) => |
104 ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
104 locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); |
105 |
105 |
106 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) |
106 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy = |
107 prmode (b, mx) (global_rhs, t') xs lthy = |
|
108 if is_locale then |
107 if is_locale then |
109 lthy |
108 lthy |
110 |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs |
109 |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs |
111 |> is_class ? Class.abbrev target prmode ((b, mx), t') |
110 |> is_class ? Class.abbrev target prmode ((b, mx), t') |
112 else |
111 else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs; |
113 lthy |
|
114 |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); |
|
115 |
112 |
116 |
113 |
117 (* declaration *) |
114 (* declaration *) |
118 |
115 |
119 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = |
116 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = |