tuned;

--- a/src/Pure/name.ML	Tue Jul 25 21:18:04 2006 +0200
+++ b/src/Pure/name.ML	Tue Jul 25 21:18:05 2006 +0200
@@ -99,8 +99,9 @@
           end;
   in invs o clean end;
 
+fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
+
 val invent_list = invents o make_context;
-fun names ctxt x xs = invents ctxt x (length xs) ~~ xs;
 
 
 (* variants *)

--- a/src/Pure/variable.ML	Tue Jul 25 21:18:04 2006 +0200
+++ b/src/Pure/variable.ML	Tue Jul 25 21:18:05 2006 +0200
@@ -297,9 +297,9 @@
 
 fun import_inst is_open ts ctxt =
   let
+    val ren = if is_open then I else Name.internal;
     val (instT, ctxt') = importT_inst ts ctxt;
     val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
-    val ren = if is_open then I else Name.internal;
     val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
     val inst = vars ~~ map Free (xs ~~ map #2 vars);
   in ((instT, inst), ctxt'') end;