diff -r a462dbaa584f -r 7849e1d10584 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -400,8 +400,8 @@
     end
   | combtyp_and_sorts_from_type (tp as TFree (a, _)) =
     (CombTFree (`make_fixed_type_var a), [tp])
-  | combtyp_and_sorts_from_type (tp as TVar (x, _)) =
-    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
+  | combtyp_and_sorts_from_type (tp as TVar (x as (s, _), _)) =
+    (CombTVar (make_schematic_type_var x, s), [tp])
 and combtyps_and_sorts_from_types Ts =
   let val (tys, ts) = ListPair.unzip (map combtyp_and_sorts_from_type Ts) in
     (tys, union_all ts)
@@ -411,8 +411,8 @@
 fun combtyp_from_typ (Type (a, Ts)) =
     CombType (`make_fixed_type_const a, map combtyp_from_typ Ts)
   | combtyp_from_typ (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
-  | combtyp_from_typ (TVar (x, _)) =
-    CombTVar (make_schematic_type_var x, string_of_indexname x)
+  | combtyp_from_typ (TVar (x as (s, _), _)) =
+    CombTVar (make_schematic_type_var x, s)
 
 fun new_skolem_const_name s num_T_args =
   [new_skolem_const_prefix, s, string_of_int num_T_args]
@@ -450,7 +450,7 @@
             val s' = new_skolem_const_name s (length tys)
           in CombConst (`make_fixed_const s', tp, map combtyp_from_typ tys) end
         else
-          CombVar ((make_schematic_var v, string_of_indexname v), tp)
+          CombVar ((make_schematic_var v, s), tp)
     in (v', ts) end
   | combterm_from_term _ bs (Bound j) =
       let