src/Pure/term.ML
changeset 20160 550e36c6a2d1
parent 20148 8a5fa86994c7
child 20199 3170fea83ae7
     1.1 --- a/src/Pure/term.ML	Wed Jul 19 12:12:02 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 19 12:12:03 2006 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4    val add_term_frees: term * term list -> term list
     1.5    val term_frees: term -> term list
     1.6    val variant_abs: string * typ * term -> string * term
     1.7 -  val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
     1.8 +  val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
     1.9    val show_question_marks: bool ref
    1.10  end;
    1.11  
    1.12 @@ -194,6 +194,7 @@
    1.13    val maxidx_term: term -> int -> int
    1.14    val declare_term_names: term -> Name.context -> Name.context
    1.15    val dest_abs: string * typ * term -> string * term
    1.16 +  val variant_frees: term -> (string * 'a) list -> (string * 'a) list
    1.17    val zero_var_indexesT: typ -> typ
    1.18    val zero_var_indexes: term -> term
    1.19    val zero_var_indexes_inst: term ->
    1.20 @@ -1161,11 +1162,10 @@
    1.21    | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    1.22    | add_term_names (_, bs) = bs;
    1.23  
    1.24 -fun declare_term_names (Const (a, _)) = Name.declare (NameSpace.base a)
    1.25 -  | declare_term_names (Free (a, _)) = Name.declare a
    1.26 -  | declare_term_names (t $ u) = declare_term_names t #> declare_term_names u
    1.27 -  | declare_term_names (Abs (_, _, t)) = declare_term_names t
    1.28 -  | declare_term_names _ = I;
    1.29 +val declare_term_names = fold_aterms
    1.30 +  (fn Const (a, _) => Name.declare (NameSpace.base a)     (*expensive*)
    1.31 +    | Free (a, _) => Name.declare a
    1.32 +    | _ => I);
    1.33  
    1.34  (*Accumulates the TVars in a type, suppressing duplicates. *)
    1.35  fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
    1.36 @@ -1255,11 +1255,13 @@
    1.37      else (x, subst_bound (Free (x, T), body))
    1.38    end;
    1.39  
    1.40 -(* renames and reverses the strings in vars away from names *)
    1.41 -fun rename_aTs names vars =
    1.42 -  rev (fst (Name.variants (map fst vars) names) ~~ map snd vars);
    1.43 +
    1.44 +(* renaming variables *)
    1.45  
    1.46 -fun rename_wrt_term t = rename_aTs (declare_term_names t Name.context);
    1.47 +fun variant_frees t frees =
    1.48 +  fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
    1.49 +
    1.50 +fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
    1.51  
    1.52  
    1.53  (* zero var indexes *)