src/Pure/variable.ML
changeset 59883 12a89103cae6
parent 59846 c7b7bca8592c
child 59884 bbf49d7dfd6f
equal deleted inserted replaced
59882:ada832308efe 59883:12a89103cae6
   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