diff -r ac069060e08a -r 41e641a870de src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Nov 10 17:47:25 2011 +0100
+++ b/src/Pure/type.ML	Thu Nov 10 22:32:10 2011 +0100
@@ -10,6 +10,7 @@
   (*constraints*)
   val mark_polymorphic: typ -> typ
   val constraint: typ -> term -> term
+  val constraint_type: Proof.context -> typ -> typ
   val strip_constraints: term -> term
   val appl_error: Proof.context -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
@@ -110,6 +111,10 @@
   if T = dummyT then t
   else Const ("_type_constraint_", T --> T) $ t;
 
+fun constraint_type ctxt T =
+  let fun err () = error ("Malformed internal type constraint: " ^ Syntax.string_of_typ ctxt T);
+  in (case T of Type ("fun", [A, B]) => if A = B then A else err () | _ => err ()) end;
+
 fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t
   | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u
   | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)