# HG changeset patch
# User wenzelm
# Date 1320703432 -3600
# Node ID 35e378c11283090f1f15464b11c809c22704deb3
# Parent  830c9b9b0d6629bdf118707c188073c58bc996d4
tuned;

diff -r 830c9b9b0d66 -r 35e378c11283 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Nov 07 21:34:11 2011 +0100
+++ b/src/Pure/variable.ML	Mon Nov 07 23:03:52 2011 +0100
@@ -403,11 +403,11 @@
 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 gen_fixes =
       Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
         (#2 (fixes_of inner)) [];
-    val still_fixed = not o member (op =) gen_fixes;
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =