--- a/src/Pure/type.ML Sun Sep 12 21:24:23 2010 +0200
+++ b/src/Pure/type.ML Sun Sep 12 22:28:59 2010 +0200
@@ -10,6 +10,7 @@
(*constraints*)
val mark_polymorphic: typ -> typ
val constraint: typ -> term -> term
+ val strip_constraints: term -> term
val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
(*type signatures and certified types*)
datatype decl =
@@ -109,6 +110,11 @@
if T = dummyT then t
else Const ("_type_constraint_", T --> T) $ t;
+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)
+ | strip_constraints a = a;
+
fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
cat_lines
["Failed to meet type constraint:", "",