1.1 --- a/src/Pure/variable.ML	Mon Nov 07 21:34:11 2011 +0100
     1.2 +++ b/src/Pure/variable.ML	Mon Nov 07 23:03:52 2011 +0100
     1.3 @@ -403,11 +403,11 @@
     1.4  fun export_inst inner outer =
     1.5    let
     1.6      val declared_outer = is_declared outer;
     1.7 +    fun still_fixed x = is_fixed outer x orelse not (is_fixed inner x);
     1.8  
     1.9      val gen_fixes =
    1.10        Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
    1.11          (#2 (fixes_of inner)) [];
    1.12 -    val still_fixed = not o member (op =) gen_fixes;
    1.13  
    1.14      val type_occs_inner = type_occs_of inner;
    1.15      fun gen_fixesT ts =