# HG changeset patch
# User wenzelm
# Date 1138881136 -3600
# Node ID 51360da418b26b24363293d6817f28293cb197c1
# Parent  9923269dcf063758e3a1c55796d9603b9a4a5c36
added specific map_typ/term (from term.ML);

diff -r 9923269dcf06 -r 51360da418b2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Feb 02 10:24:06 2006 +0100
+++ b/src/Pure/sign.ML	Thu Feb 02 12:52:16 2006 +0100
@@ -309,6 +309,17 @@
 
 local
 
+fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
+  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
+  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
+
+fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
+  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
+  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
+  | map_term _ _ _ (t as Bound _) = t
+  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
+  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
+
 fun mapping add_names f t =
   let
     fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
@@ -317,12 +328,12 @@
   in get end;
 
 fun typ_mapping f g thy T =
-  T |> Term.map_typ
+  T |> map_typ
     (mapping add_typ_classes (f thy) T)
     (mapping add_typ_tycons (g thy) T);
 
 fun term_mapping f g h thy t =
-  t |> Term.map_term
+  t |> map_term
     (mapping add_term_classes (f thy) t)
     (mapping add_term_tycons (g thy) t)
     (mapping add_term_consts (h thy) t);