src/Pure/term.ML
changeset 16338 3d1851acb4d0
parent 16294 97c9f2c1de3d
child 16537 954495db0f07
     1.1 --- a/src/Pure/term.ML	Thu Jun 09 12:03:24 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jun 09 12:03:25 2005 +0200
     1.3 @@ -70,10 +70,6 @@
     1.4    val map_type_tfree: (string * sort -> typ) -> typ -> typ
     1.5    val map_term_types: (typ -> typ) -> term -> term
     1.6    val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
     1.7 -  val map_typ: (class -> class) -> (string -> string) -> typ -> typ
     1.8 -  val map_term:
     1.9 -     (class -> class) ->
    1.10 -     (string -> string) -> (string -> string) -> term -> term
    1.11    val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
    1.12    val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
    1.13    val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
    1.14 @@ -178,6 +174,8 @@
    1.15    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    1.16    val rename_abs: term -> term -> term -> term option
    1.17    val invent_names: string list -> string -> int -> string list
    1.18 +  val map_typ: (string -> string) -> (string -> string) -> typ -> typ
    1.19 +  val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
    1.20    val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
    1.21    val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
    1.22    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
    1.23 @@ -1058,6 +1056,7 @@
    1.24       it should be called only for axioms, stored theorems, etc.
    1.25       Recorded term and type fragments are never disposed. ***)
    1.26  
    1.27 +
    1.28  (** Sharing of types **)
    1.29  
    1.30  val memo_types = ref (Typtab.empty: typ Typtab.table);