# HG changeset patch
# User wenzelm
# Date 1118311405 -7200
# Node ID 3d1851acb4d08108f4f44a4093f291496e26d8f4
# Parent  5734de2f7acee8ca42d9368e78eb1c1ef5ce2f63
map_typ and map_term no longer global;

diff -r 5734de2f7ace -r 3d1851acb4d0 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Jun 09 12:03:24 2005 +0200
+++ b/src/Pure/term.ML	Thu Jun 09 12:03:25 2005 +0200
@@ -70,10 +70,6 @@
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
   val map_term_types: (typ -> typ) -> term -> term
   val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
-  val map_typ: (class -> class) -> (string -> string) -> typ -> typ
-  val map_term:
-     (class -> class) ->
-     (string -> string) -> (string -> string) -> term -> term
   val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
   val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
   val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
@@ -178,6 +174,8 @@
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
   val rename_abs: term -> term -> term -> term option
   val invent_names: string list -> string -> int -> string list
+  val map_typ: (string -> string) -> (string -> string) -> typ -> typ
+  val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
   val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   val add_vars: (indexname * typ) list * term -> (indexname * typ) list
@@ -1058,6 +1056,7 @@
      it should be called only for axioms, stored theorems, etc.
      Recorded term and type fragments are never disposed. ***)
 
+
 (** Sharing of types **)
 
 val memo_types = ref (Typtab.empty: typ Typtab.table);