# HG changeset patch # User wenzelm # Date 1153245704 -7200 # Node ID 8a5fa86994c72a8615c796f5946f5f25c2bccd38 # Parent 7aa076a45cb436e4215c1c3cfd7a5f4579af1d71 added declare_term_names; tuned; diff -r 7aa076a45cb4 -r 8a5fa86994c7 src/Pure/term.ML --- a/src/Pure/term.ML Tue Jul 18 20:01:42 2006 +0200 +++ b/src/Pure/term.ML Tue Jul 18 20:01:44 2006 +0200 @@ -192,6 +192,7 @@ val maxidx_typ: typ -> int -> int val maxidx_typs: typ list -> int -> int val maxidx_term: term -> int -> int + val declare_term_names: term -> Name.context -> Name.context val dest_abs: string * typ * term -> string * term val zero_var_indexesT: typ -> typ val zero_var_indexes: term -> term @@ -1160,6 +1161,12 @@ | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) | add_term_names (_, bs) = bs; +fun declare_term_names (Const (a, _)) = Name.declare (NameSpace.base a) + | declare_term_names (Free (a, _)) = Name.declare a + | declare_term_names (t $ u) = declare_term_names t #> declare_term_names u + | declare_term_names (Abs (_, _, t)) = declare_term_names t + | declare_term_names _ = I; + (*Accumulates the TVars in a type, suppressing duplicates. *) fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts | add_typ_tvars(TFree(_),vs) = vs @@ -1232,9 +1239,9 @@ (*Given an abstraction over P, replaces the bound variable by a Free variable having a unique name -- SLOW!*) -fun variant_abs (a,T,P) = - let val b = Name.variant (add_term_names(P,[])) a - in (b, subst_bound (Free(b,T), P)) end; +fun variant_abs (x, T, b) = + let val ([x'], _) = Name.variants [x] (declare_term_names b Name.context) + in (x', subst_bound (Free (x', T), b)) end; fun dest_abs (x, T, body) = let @@ -1249,12 +1256,10 @@ end; (* renames and reverses the strings in vars away from names *) -fun rename_aTs names vars : (string*typ)list = - let fun rename_aT (vars,(a,T)) = - (Name.variant (map #1 vars @ names) a, T) :: vars - in Library.foldl rename_aT ([],vars) end; +fun rename_aTs names vars = + rev (fst (Name.variants (map fst vars) names) ~~ map snd vars); -fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); +fun rename_wrt_term t = rename_aTs (declare_term_names t Name.context); (* zero var indexes *)