73 else Generic_Target.theory_notes; |
73 else Generic_Target.theory_notes; |
74 |
74 |
75 |
75 |
76 (* abbrev *) |
76 (* abbrev *) |
77 |
77 |
78 fun locale_abbrev locale prmode (b, mx) (t, _) xs = |
78 fun locale_abbrev locale prmode (b, mx) (global_rhs, _) params = |
79 Generic_Target.background_abbrev (b, t) xs |
79 Generic_Target.background_abbrev (b, global_rhs) params |
80 #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs)); |
80 #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs)); |
81 |
81 |
82 fun class_abbrev class prmode (b, mx) (t, t') xs = |
82 fun class_abbrev class prmode (b, mx) (global_rhs, rhs') params = |
83 Generic_Target.background_abbrev (b, t) xs |
83 Generic_Target.background_abbrev (b, global_rhs) params |
84 #-> (fn (lhs, _) => Class.abbrev class prmode ((b, mx), lhs) t'); |
84 #-> (fn (lhs, _) => Class.abbrev class prmode ((b, mx), lhs) rhs'); |
85 |
85 |
86 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = |
86 fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = |
87 if is_class then class_abbrev target |
87 if is_class then class_abbrev target |
88 else if is_locale then locale_abbrev target |
88 else if is_locale then locale_abbrev target |
89 else Generic_Target.theory_abbrev; |
89 else Generic_Target.theory_abbrev; |