# HG changeset patch
# User wenzelm
# Date 1152651637 -7200
# Node ID c96cb48eef530f93f9e5fecc3c23d1e20c68fa2c
# Parent  bc3f9cb336458d12113c7ab8a7e016836286b575
removed obsolete xless;
tuned zero_var_indexes;

diff -r bc3f9cb33645 -r c96cb48eef53 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Jul 11 23:00:36 2006 +0200
+++ b/src/Pure/term.ML	Tue Jul 11 23:00:37 2006 +0200
@@ -103,7 +103,6 @@
   val eq_ix: indexname * indexname -> bool
   val could_unify: term * term -> bool
   val subst_free: (term * term) list -> term -> term
-  val xless: (string * int) * indexname -> bool
   val abstract_over: term * term -> term
   val lambda: term -> term -> term
   val absfree: string * typ * term -> term
@@ -853,10 +852,6 @@
                                  | _ => u)
       in  substf  end;
 
-(*a total, irreflexive ordering on index names*)
-fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
-
-
 (*Abstraction of the term "body" over its occurrences of v,
     which must contain no loose bound variables.
   The resulting term is ready to become the body of an Abs.*)
@@ -928,7 +923,6 @@
 fun subst_TVars [] tm = tm
   | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
 
-(*see also Envir.norm_term*)
 fun subst_Vars [] tm = tm
   | subst_Vars inst tm =
       let
@@ -938,7 +932,6 @@
           | subst t = t;
       in subst tm end;
 
-(*see also Envir.norm_term*)
 fun subst_vars ([], []) tm = tm
   | subst_vars ([], inst) tm = subst_Vars inst tm
   | subst_vars (instT, inst) tm =
@@ -1241,10 +1234,9 @@
 fun zero_var_inst vars =
   fold (fn v as ((x, i), X) => fn (used, inst) =>
     let
-      val x' = Name.variant used (if Name.is_bound x then "u" else x);
-      val used' = x' :: used;
+      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
-  vars ([], []) |> #2;
+  vars (Name.context, []) |> #2;
 
 fun zero_var_indexesT ty =
   instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
@@ -1305,6 +1297,8 @@
   in (subst_atomic insts tm, xs) end;
 
 
+(* display variables *)
+
 val show_question_marks = ref true;
 
 fun string_of_vname (x, i) =