# HG changeset patch
# User wenzelm
# Date 1164402316 -3600
# Node ID 63c73f461eec7a093b54baa353db3b1bd3f0ee73
# Parent  33f109ea389f630f2aeccb088c60c76eb93710f6
added type_map;

diff -r 33f109ea389f -r 63c73f461eec src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Nov 24 22:05:15 2006 +0100
+++ b/src/Pure/logic.ML	Fri Nov 24 22:05:16 2006 +0100
@@ -28,7 +28,9 @@
   val dest_conjunction_list: term -> term list
   val dest_conjunctions: term -> term list
   val strip_horn: term -> term list * term
+  val mk_type: typ -> term
   val dest_type: term -> typ
+  val type_map: (term -> term) -> typ -> typ
   val const_of_class: class -> string
   val class_of_const: string -> class
   val mk_inclass: typ * class -> term
@@ -45,7 +47,6 @@
   val abs_def: term -> term * term
   val mk_cond_defpair: term list -> term * term -> string * term
   val mk_defpair: term * term -> string * term
-  val mk_type: typ -> term
   val protectC: term
   val protect: term -> term
   val unprotect: term -> term
@@ -189,6 +190,8 @@
 fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty
   | dest_type t = raise TERM ("dest_type", [t]);
 
+fun type_map f = dest_type o f o mk_type;
+
 
 
 (** type classes **)