187 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi = |
187 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi = |
188 let |
188 let |
189 val c' = Morphism.name phi c; |
189 val c' = Morphism.name phi c; |
190 val rhs' = Morphism.term phi rhs; |
190 val rhs' = Morphism.term phi rhs; |
191 val name = Name.name_of c; |
191 val name = Name.name_of c; |
192 val name' = Name.name_of c' |
192 val name' = Name.name_of c'; |
193 val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs')); |
193 val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs')); |
194 val arg = (name', Term.close_schematic_term rhs'); |
194 val arg = (name', Term.close_schematic_term rhs'); |
195 val similar_body = Type.similar_types (rhs, rhs'); |
195 val similar_body = Type.similar_types (rhs, rhs'); |
196 (* FIXME workaround based on educated guess *) |
196 (* FIXME workaround based on educated guess *) |
197 val class_global = name' = NameSpace.qualified (Class.class_prefix target) name; |
197 val class_global = name = NameSpace.base name' |
|
198 andalso Class.class_prefix target = hd (NameSpace.explode name'); |
198 in |
199 in |
199 not (is_class andalso (similar_body orelse class_global)) ? |
200 not (is_class andalso (similar_body orelse class_global)) ? |
200 (Context.mapping_result |
201 (Context.mapping_result |
201 (Sign.add_abbrev PrintMode.internal tags legacy_arg) |
202 (Sign.add_abbrev PrintMode.internal tags legacy_arg) |
202 (ProofContext.add_abbrev PrintMode.internal tags arg) |
203 (ProofContext.add_abbrev PrintMode.internal tags arg) |