removed obsolete xless;
authorwenzelm
Tue Jul 11 23:00:37 2006 +0200 (2006-07-11)
changeset 20100c96cb48eef53
parent 20099 bc3f9cb33645
child 20101 a8d73903dc72
removed obsolete xless;
tuned zero_var_indexes;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Jul 11 23:00:36 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Jul 11 23:00:37 2006 +0200
     1.3 @@ -103,7 +103,6 @@
     1.4    val eq_ix: indexname * indexname -> bool
     1.5    val could_unify: term * term -> bool
     1.6    val subst_free: (term * term) list -> term -> term
     1.7 -  val xless: (string * int) * indexname -> bool
     1.8    val abstract_over: term * term -> term
     1.9    val lambda: term -> term -> term
    1.10    val absfree: string * typ * term -> term
    1.11 @@ -853,10 +852,6 @@
    1.12                                   | _ => u)
    1.13        in  substf  end;
    1.14  
    1.15 -(*a total, irreflexive ordering on index names*)
    1.16 -fun xless ((a,i), (b,j): indexname) = i<j  orelse  (i=j andalso a<b);
    1.17 -
    1.18 -
    1.19  (*Abstraction of the term "body" over its occurrences of v,
    1.20      which must contain no loose bound variables.
    1.21    The resulting term is ready to become the body of an Abs.*)
    1.22 @@ -928,7 +923,6 @@
    1.23  fun subst_TVars [] tm = tm
    1.24    | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
    1.25  
    1.26 -(*see also Envir.norm_term*)
    1.27  fun subst_Vars [] tm = tm
    1.28    | subst_Vars inst tm =
    1.29        let
    1.30 @@ -938,7 +932,6 @@
    1.31            | subst t = t;
    1.32        in subst tm end;
    1.33  
    1.34 -(*see also Envir.norm_term*)
    1.35  fun subst_vars ([], []) tm = tm
    1.36    | subst_vars ([], inst) tm = subst_Vars inst tm
    1.37    | subst_vars (instT, inst) tm =
    1.38 @@ -1241,10 +1234,9 @@
    1.39  fun zero_var_inst vars =
    1.40    fold (fn v as ((x, i), X) => fn (used, inst) =>
    1.41      let
    1.42 -      val x' = Name.variant used (if Name.is_bound x then "u" else x);
    1.43 -      val used' = x' :: used;
    1.44 +      val ([x'], used') = Name.variants [if Name.is_bound x then "u" else x] used;
    1.45      in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
    1.46 -  vars ([], []) |> #2;
    1.47 +  vars (Name.context, []) |> #2;
    1.48  
    1.49  fun zero_var_indexesT ty =
    1.50    instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty;
    1.51 @@ -1305,6 +1297,8 @@
    1.52    in (subst_atomic insts tm, xs) end;
    1.53  
    1.54  
    1.55 +(* display variables *)
    1.56 +
    1.57  val show_question_marks = ref true;
    1.58  
    1.59  fun string_of_vname (x, i) =