--- 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)