# HG changeset patch
# User wenzelm
# Date 1153855085 -7200
# Node ID 7b385487f22fdc0415883150b6a8982fcf6035d6
# Parent  ffc64d90fc1f06842cd135dcff20aebcefbf16dd
tuned;

diff -r ffc64d90fc1f -r 7b385487f22f src/Pure/name.ML
--- 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 *)
diff -r ffc64d90fc1f -r 7b385487f22f src/Pure/variable.ML
--- 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;