| changeset 59883 | 12a89103cae6 |
| parent 59846 | c7b7bca8592c |
| child 59884 | bbf49d7dfd6f |
--- a/src/Pure/variable.ML Tue Mar 31 19:39:05 2015 +0200 +++ b/src/Pure/variable.ML Tue Mar 31 20:07:37 2015 +0200 @@ -347,7 +347,7 @@ (* specialized name space *) -val is_fixed = Name_Space.defined_entry o fixes_space; +val is_fixed = Name_Space.defined o fixes_of; fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer); val fixed_ord = Name_Space.entry_ord o fixes_space;