--- a/src/Pure/type_infer.ML Fri May 05 21:59:44 2006 +0200
+++ b/src/Pure/type_infer.ML Fri May 05 21:59:45 2006 +0200
@@ -173,7 +173,8 @@
(ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
| pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
| pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
- | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
+ | pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) =
+ constrain (pre_of (ps, t)) T
| pre_of (ps, Bound i) = (ps, PBound i)
| pre_of (ps, Abs (x, T, t)) =
let
@@ -431,7 +432,7 @@
fun constrain t T =
if T = dummyT then t
- else Const ("_type_constraint_", T) $ t;
+ else Const ("_type_constraint_", T --> T) $ t;
(* user parameters *)