# HG changeset patch
# User wenzelm
# Date 1130939335 -3600
# Node ID 16608ab6ed84c26e21535e3834d0842542eb1a6c
# Parent  f5727fa16c77921760f88f3a9ba694ca85992e46
removed unused modify_typargs, map_typargs, fold_typargs;

diff -r f5727fa16c77 -r 16608ab6ed84 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Nov 02 14:47:01 2005 +0100
+++ b/src/Pure/consts.ML	Wed Nov 02 14:48:55 2005 +0100
@@ -14,9 +14,6 @@
   val constraint: T -> string -> typ    (*exception TYPE*)
   val monomorphic: T -> string -> bool
   val typargs: T -> string -> typ -> typ list
-  val modify_typargs: T -> string -> (typ list -> typ list) -> typ -> typ
-  val map_typargs: T -> string -> (typ -> typ) -> typ -> typ
-  val fold_typargs: T -> string -> (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val declare: NameSpace.naming -> bstring * typ -> T -> T
   val constrain: string * typ -> T -> T
   val hide: bool -> string -> T -> T
@@ -75,27 +72,6 @@
   let val (_, args) = the_const consts c
   in fn T => map (sub T o #2) args end;
 
-fun modify_typargs consts c =
-  let val (declT, args) = the_const consts c in
-    fn f => fn T =>
-      let
-        val Us = f (map (sub T o #2) args);
-        val _ =
-          if length args = length Us then ()
-          else raise TYPE ("modify_typargs: bad number of args", [T], []);
-        val inst = ListPair.map (fn ((v, _), U) => (v, U)) (args, Us);
-      in declT |> Term.instantiateT inst end
-  end;
-
-fun map_typargs consts c =
-  let val (declT, args) = the_const consts c in
-    fn f => fn T => declT |> Term.instantiateT (args |> map (fn (v, pos) => (v, f (sub T pos))))
-  end;
-
-fun fold_typargs consts c =
-  let val (_, args) = the_const consts c
-  in fn f => fn T => fold (f o sub T o #2) args end;
-
 
 
 (** build consts **)