src/Pure/term.ML
changeset 14695 9c78044b99c3
parent 14676 82721f31de3e
child 14786 24a7bc97a27a
equal deleted inserted replaced
14694:49873d345a39 14695:9c78044b99c3
   179 sig
   179 sig
   180   include BASIC_TERM
   180   include BASIC_TERM
   181   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   181   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   182   val rename_abs: term -> term -> term -> term option
   182   val rename_abs: term -> term -> term -> term option
   183   val invent_names: string list -> string -> int -> string list
   183   val invent_names: string list -> string -> int -> string list
   184   val invent_type_names: string list -> int -> string list
       
   185   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   184   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   186   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   185   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   187   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   186   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   188   val add_frees: (string * typ) list * term -> (string * typ) list
   187   val add_frees: (string * typ) list * term -> (string * typ) list
   189   val indexname_ord: indexname * indexname -> order
   188   val indexname_ord: indexname * indexname -> order
   771 fun variantlist ([], used) = []
   770 fun variantlist ([], used) = []
   772   | variantlist(b::bs, used) =
   771   | variantlist(b::bs, used) =
   773       let val b' = variant used b
   772       let val b' = variant used b
   774       in  b' :: variantlist (bs, b'::used)  end;
   773       in  b' :: variantlist (bs, b'::used)  end;
   775 
   774 
   776 fun invent_names used prfx n = variantlist (Library.replicate n prfx, prfx :: used);
   775 (*Invent fresh names*)
   777 fun invent_type_names used = invent_names used "'";
   776 fun invent_names _ _ 0 = []
       
   777   | invent_names used a n =
       
   778       let val b = Symbol.bump_string a in
       
   779         if a mem_string used then invent_names used b n
       
   780         else a :: invent_names used b (n - 1)
       
   781       end;
   778 
   782 
   779 
   783 
   780 
   784 
   781 (** Consts etc. **)
   785 (** Consts etc. **)
   782 
   786