# HG changeset patch # User wenzelm # Date 1230749644 -3600 # Node ID e9d148a808eb4c42371ed6f44bce5f9fe4baaeb0 # Parent 29dd1c516337bfaa8abfb3acb0bc93af72023378 added declare_term_frees; tuned signature; diff -r 29dd1c516337 -r e9d148a808eb src/Pure/term.ML --- a/src/Pure/term.ML Wed Dec 31 19:54:04 2008 +0100 +++ b/src/Pure/term.ML Wed Dec 31 19:54:04 2008 +0100 @@ -110,7 +110,6 @@ val exists_type: (typ -> bool) -> term -> bool val exists_subterm: (term -> bool) -> term -> bool val exists_Const: (string * typ -> bool) -> term -> bool - val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list val show_question_marks: bool ref end; @@ -135,6 +134,11 @@ val add_free_names: term -> string list -> string list val add_frees: term -> (string * typ) list -> (string * typ) list val hidden_polymorphism: term -> (indexname * sort) list + val declare_typ_names: typ -> Name.context -> Name.context + val declare_term_names: term -> Name.context -> Name.context + val declare_term_frees: term -> Name.context -> Name.context + val variant_frees: term -> (string * 'a) list -> (string * 'a) list + val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list val eq_ix: indexname * indexname -> bool val eq_tvar: (indexname * sort) * (indexname * sort) -> bool val eq_var: (indexname * typ) * (indexname * typ) -> bool @@ -149,9 +153,6 @@ val maxidx_term: term -> int -> int val has_abs: term -> bool val dest_abs: string * typ * term -> string * term - val declare_typ_names: typ -> Name.context -> Name.context - val declare_term_names: term -> Name.context -> Name.context - val variant_frees: term -> (string * 'a) list -> (string * 'a) list val dummy_patternN: string val dummy_pattern: typ -> term val is_dummy_pattern: term -> bool @@ -470,6 +471,25 @@ in extra_tvars end; +(* renaming variables *) + +val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); + +fun declare_term_names tm = + fold_aterms + (fn Const (a, _) => Name.declare (NameSpace.base a) + | Free (a, _) => Name.declare a + | _ => I) tm #> + fold_types declare_typ_names tm; + +val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I); + +fun variant_frees t frees = + fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; + +fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) + + (** Comparing terms **) @@ -638,7 +658,7 @@ of bound variables and implicit eta-expansion*) fun strip_abs_eta k t = let - val used = fold_aterms (fn Free (v, _) => Name.declare v | _ => I) t Name.context; + val used = fold_aterms declare_term_frees t Name.context; fun strip_abs t (0, used) = (([], t), (0, used)) | strip_abs (Abs (v, T, t)) (k, used) = let @@ -876,23 +896,6 @@ end; -(* renaming variables *) - -val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I); - -fun declare_term_names tm = - fold_aterms - (fn Const (a, _) => Name.declare (NameSpace.base a) - | Free (a, _) => Name.declare a - | _ => I) tm #> - fold_types declare_typ_names tm; - -fun variant_frees t frees = - fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; - -fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) - - (* dummy patterns *) val dummy_patternN = "dummy_pattern";