added declare_term_names;
authorwenzelm
Tue Jul 18 20:01:44 2006 +0200 (2006-07-18)
changeset 201488a5fa86994c7
parent 20147 7aa076a45cb4
child 20149 54d4ea7927be
added declare_term_names;
tuned;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Jul 18 20:01:42 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Jul 18 20:01:44 2006 +0200
     1.3 @@ -192,6 +192,7 @@
     1.4    val maxidx_typ: typ -> int -> int
     1.5    val maxidx_typs: typ list -> int -> int
     1.6    val maxidx_term: term -> int -> int
     1.7 +  val declare_term_names: term -> Name.context -> Name.context
     1.8    val dest_abs: string * typ * term -> string * term
     1.9    val zero_var_indexesT: typ -> typ
    1.10    val zero_var_indexes: term -> term
    1.11 @@ -1160,6 +1161,12 @@
    1.12    | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    1.13    | add_term_names (_, bs) = bs;
    1.14  
    1.15 +fun declare_term_names (Const (a, _)) = Name.declare (NameSpace.base a)
    1.16 +  | declare_term_names (Free (a, _)) = Name.declare a
    1.17 +  | declare_term_names (t $ u) = declare_term_names t #> declare_term_names u
    1.18 +  | declare_term_names (Abs (_, _, t)) = declare_term_names t
    1.19 +  | declare_term_names _ = I;
    1.20 +
    1.21  (*Accumulates the TVars in a type, suppressing duplicates. *)
    1.22  fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
    1.23    | add_typ_tvars(TFree(_),vs) = vs
    1.24 @@ -1232,9 +1239,9 @@
    1.25  
    1.26  (*Given an abstraction over P, replaces the bound variable by a Free variable
    1.27    having a unique name -- SLOW!*)
    1.28 -fun variant_abs (a,T,P) =
    1.29 -  let val b = Name.variant (add_term_names(P,[])) a
    1.30 -  in  (b,  subst_bound (Free(b,T), P))  end;
    1.31 +fun variant_abs (x, T, b) =
    1.32 +  let val ([x'], _) = Name.variants [x] (declare_term_names b Name.context)
    1.33 +  in (x', subst_bound (Free (x', T), b))  end;
    1.34  
    1.35  fun dest_abs (x, T, body) =
    1.36    let
    1.37 @@ -1249,12 +1256,10 @@
    1.38    end;
    1.39  
    1.40  (* renames and reverses the strings in vars away from names *)
    1.41 -fun rename_aTs names vars : (string*typ)list =
    1.42 -  let fun rename_aT (vars,(a,T)) =
    1.43 -                (Name.variant (map #1 vars @ names) a, T) :: vars
    1.44 -  in Library.foldl rename_aT ([],vars) end;
    1.45 +fun rename_aTs names vars =
    1.46 +  rev (fst (Name.variants (map fst vars) names) ~~ map snd vars);
    1.47  
    1.48 -fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
    1.49 +fun rename_wrt_term t = rename_aTs (declare_term_names t Name.context);
    1.50  
    1.51  
    1.52  (* zero var indexes *)