--- 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) =