equal
deleted
inserted
replaced
229 (* name space aliases *) |
229 (* name space aliases *) |
230 |
230 |
231 fun alias global_alias local_alias b name = |
231 fun alias global_alias local_alias b name = |
232 declaration {syntax = true, pervasive = false} (fn phi => |
232 declaration {syntax = true, pervasive = false} (fn phi => |
233 let val b' = Morphism.binding phi b |
233 let val b' = Morphism.binding phi b |
234 in Context.mapping (global_alias b' name) (local_alias b' name) end) |
234 in Context.mapping (global_alias b' name) (local_alias b' name) end); |
235 #> local_alias b name; |
|
236 |
235 |
237 val class_alias = alias Sign.class_alias Proof_Context.class_alias; |
236 val class_alias = alias Sign.class_alias Proof_Context.class_alias; |
238 val type_alias = alias Sign.type_alias Proof_Context.type_alias; |
237 val type_alias = alias Sign.type_alias Proof_Context.type_alias; |
239 val const_alias = alias Sign.const_alias Proof_Context.const_alias; |
238 val const_alias = alias Sign.const_alias Proof_Context.const_alias; |
240 |
239 |