184 |
184 |
185 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi = |
185 fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((c, mx), rhs) phi = |
186 let |
186 let |
187 val c' = Morphism.name phi c; |
187 val c' = Morphism.name phi c; |
188 val rhs' = Morphism.term phi rhs; |
188 val rhs' = Morphism.term phi rhs; |
189 val name' = Name.name_of c'; |
189 val name' = Name.name_with_prefix c'; |
190 val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs')); |
190 val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs')); |
191 val arg = (name', Term.close_schematic_term rhs'); |
191 val arg = (name', Term.close_schematic_term rhs'); |
192 val similar_body = Type.similar_types (rhs, rhs'); |
192 val similar_body = Type.similar_types (rhs, rhs'); |
193 (* FIXME workaround based on educated guess *) |
193 (* FIXME workaround based on educated guess *) |
194 val class_global = Name.name_of c = Name.name_of c' |
194 val class_global = Name.name_of c = Name.name_of c' |
195 andalso not (null (Name.prefix_of c')) |
195 andalso not (null (Name.prefix_of c')) |
196 andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target; |
196 andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target; |
197 in |
197 in |
198 not (is_class andalso (similar_body orelse class_global)) ? |
198 not (is_class andalso (similar_body orelse class_global)) ? |
199 (Context.mapping_result |
199 (Context.mapping_result |
200 (Sign.add_abbrev PrintMode.internal tags legacy_arg) |
200 (fn thy => thy |> |
|
201 Sign.no_base_names |
|
202 |> Sign.add_abbrev PrintMode.internal tags legacy_arg |
|
203 ||> Sign.restore_naming thy) |
201 (ProofContext.add_abbrev PrintMode.internal tags arg) |
204 (ProofContext.add_abbrev PrintMode.internal tags arg) |
202 #-> (fn (lhs' as Const (d, _), _) => |
205 #-> (fn (lhs' as Const (d, _), _) => |
203 similar_body ? |
206 similar_body ? |
204 (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #> |
207 (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #> |
205 Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) |
208 Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) |