equal
deleted
inserted
replaced
345 | NONE => false); |
345 | NONE => false); |
346 |
346 |
347 |
347 |
348 (* specialized name space *) |
348 (* specialized name space *) |
349 |
349 |
350 val is_fixed = Name_Space.defined_entry o fixes_space; |
350 val is_fixed = Name_Space.defined o fixes_of; |
351 fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); |
351 fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); |
352 |
352 |
353 val fixed_ord = Name_Space.entry_ord o fixes_space; |
353 val fixed_ord = Name_Space.entry_ord o fixes_space; |
354 val intern_fixed = Name_Space.intern o fixes_space; |
354 val intern_fixed = Name_Space.intern o fixes_space; |
355 |
355 |