diff -r ada832308efe -r 12a89103cae6 src/Pure/variable.ML --- 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;