1.1 --- a/src/Pure/consts.ML	Wed Nov 02 14:47:01 2005 +0100
     1.2 +++ b/src/Pure/consts.ML	Wed Nov 02 14:48:55 2005 +0100
     1.3 @@ -14,9 +14,6 @@
     1.4    val constraint: T -> string -> typ    (*exception TYPE*)
     1.5    val monomorphic: T -> string -> bool
     1.6    val typargs: T -> string -> typ -> typ list
     1.7 -  val modify_typargs: T -> string -> (typ list -> typ list) -> typ -> typ
     1.8 -  val map_typargs: T -> string -> (typ -> typ) -> typ -> typ
     1.9 -  val fold_typargs: T -> string -> (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    1.10    val declare: NameSpace.naming -> bstring * typ -> T -> T
    1.11    val constrain: string * typ -> T -> T
    1.12    val hide: bool -> string -> T -> T
    1.13 @@ -75,27 +72,6 @@
    1.14    let val (_, args) = the_const consts c
    1.15    in fn T => map (sub T o #2) args end;
    1.16  
    1.17 -fun modify_typargs consts c =
    1.18 -  let val (declT, args) = the_const consts c in
    1.19 -    fn f => fn T =>
    1.20 -      let
    1.21 -        val Us = f (map (sub T o #2) args);
    1.22 -        val _ =
    1.23 -          if length args = length Us then ()
    1.24 -          else raise TYPE ("modify_typargs: bad number of args", [T], []);
    1.25 -        val inst = ListPair.map (fn ((v, _), U) => (v, U)) (args, Us);
    1.26 -      in declT |> Term.instantiateT inst end
    1.27 -  end;
    1.28 -
    1.29 -fun map_typargs consts c =
    1.30 -  let val (declT, args) = the_const consts c in
    1.31 -    fn f => fn T => declT |> Term.instantiateT (args |> map (fn (v, pos) => (v, f (sub T pos))))
    1.32 -  end;
    1.33 -
    1.34 -fun fold_typargs consts c =
    1.35 -  let val (_, args) = the_const consts c
    1.36 -  in fn f => fn T => fold (f o sub T o #2) args end;
    1.37 -
    1.38  
    1.39  
    1.40  (** build consts **)