src/Pure/logic.ML
changeset 21520 63c73f461eec
parent 21016 430b35c9cd27
child 21576 8c11b1ce2f05
     1.1 --- a/src/Pure/logic.ML	Fri Nov 24 22:05:15 2006 +0100
     1.2 +++ b/src/Pure/logic.ML	Fri Nov 24 22:05:16 2006 +0100
     1.3 @@ -28,7 +28,9 @@
     1.4    val dest_conjunction_list: term -> term list
     1.5    val dest_conjunctions: term -> term list
     1.6    val strip_horn: term -> term list * term
     1.7 +  val mk_type: typ -> term
     1.8    val dest_type: term -> typ
     1.9 +  val type_map: (term -> term) -> typ -> typ
    1.10    val const_of_class: class -> string
    1.11    val class_of_const: string -> class
    1.12    val mk_inclass: typ * class -> term
    1.13 @@ -45,7 +47,6 @@
    1.14    val abs_def: term -> term * term
    1.15    val mk_cond_defpair: term list -> term * term -> string * term
    1.16    val mk_defpair: term * term -> string * term
    1.17 -  val mk_type: typ -> term
    1.18    val protectC: term
    1.19    val protect: term -> term
    1.20    val unprotect: term -> term
    1.21 @@ -189,6 +190,8 @@
    1.22  fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
    1.23    | dest_type t = raise TERM ("dest_type", [t]);
    1.24  
    1.25 +fun type_map f = dest_type o f o mk_type;
    1.26 +
    1.27  
    1.28  
    1.29  (** type classes **)