more direct Name_Space.defined_entry;
tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

--- a/src/Pure/General/name_space.ML	Sun Mar 11 13:54:08 2012 +0100
+++ b/src/Pure/General/name_space.ML	Sun Mar 11 14:09:01 2012 +0100
@@ -14,6 +14,7 @@
   type T
   val empty: string -> T
   val kind_of: T -> string
+  val defined_entry: T -> string -> bool
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, id: serial}
   val entry_ord: T -> string * string -> order
@@ -117,6 +118,8 @@
 
 fun kind_of (Name_Space {kind, ...}) = kind;
 
+fun defined_entry (Name_Space {entries, ...}) = Symtab.defined entries;
+
 fun the_entry (Name_Space {kind, entries, ...}) name =
   (case Symtab.lookup entries name of
     NONE => error ("Unknown " ^ kind ^ " " ^ quote name)

--- a/src/Pure/variable.ML	Sun Mar 11 13:54:08 2012 +0100
+++ b/src/Pure/variable.ML	Sun Mar 11 14:09:01 2012 +0100
@@ -292,8 +292,8 @@
 
 (* specialized name space *)
 
-fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
-fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
+val is_fixed = Name_Space.defined_entry o fixes_space;
+fun newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
@@ -406,7 +406,7 @@
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
-    fun still_fixed x = is_fixed outer x orelse not (is_fixed inner x);
+    val still_fixed = not o newly_fixed inner outer;
 
     val gen_fixes =
       Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)