src/Pure/term.ML
changeset 20100 c96cb48eef53
parent 20082 b0f5981b9267
child 20109 47fef41c68fb
     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) =