# HG changeset patch
# User wenzelm
# Date 1208463746 -7200
# Node ID 4773b832f1b1208e1ab41791cfe60f2f09528af5
# Parent  1c6181def1d0812eb16a468f33b52923b2f3168c
variant_fixes: preserve internal state, mark skolem only for body mode;
import_inst: actually observe is_open flag (cf. variant_fixes);

diff -r 1c6181def1d0 -r 4773b832f1b1 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Apr 17 22:22:25 2008 +0200
+++ b/src/Pure/variable.ML	Thu Apr 17 22:22:26 2008 +0200
@@ -300,8 +300,8 @@
 fun variant_fixes raw_xs ctxt =
   let
     val names = names_of ctxt;
-    val xs = map Name.clean raw_xs;
-    val (xs', names') = Name.variants xs names |>> map Name.skolem;
+    val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
+    val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
   in ctxt |> new_fixes names' xs xs' end;
 
 end;
@@ -401,7 +401,7 @@
 
 fun import_inst is_open ts ctxt =
   let
-    val ren = if is_open then I else Name.internal;
+    val ren = Name.clean #> (if is_open then I else Name.internal);
     val (instT, ctxt') = importT_inst ts ctxt;
     val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
     val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';