src/Pure/type.ML
changeset 39292 6f085332c7d3
parent 39290 44e4d8dfd6bf
child 39997 b654fa27fbc4
     1.1 --- a/src/Pure/type.ML	Sun Sep 12 21:24:23 2010 +0200
     1.2 +++ b/src/Pure/type.ML	Sun Sep 12 22:28:59 2010 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    (*constraints*)
     1.5    val mark_polymorphic: typ -> typ
     1.6    val constraint: typ -> term -> term
     1.7 +  val strip_constraints: term -> term
     1.8    val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
     1.9    (*type signatures and certified types*)
    1.10    datatype decl =
    1.11 @@ -109,6 +110,11 @@
    1.12    if T = dummyT then t
    1.13    else Const ("_type_constraint_", T --> T) $ t;
    1.14  
    1.15 +fun strip_constraints (Const ("_type_constraint_", _) $ t) = strip_constraints t
    1.16 +  | strip_constraints (t $ u) = strip_constraints t $ strip_constraints u
    1.17 +  | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
    1.18 +  | strip_constraints a = a;
    1.19 +
    1.20  fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
    1.21        cat_lines
    1.22         ["Failed to meet type constraint:", "",