src/Pure/type_infer.ML
changeset 19577 fdb3642feb49
parent 19482 9f11af8f7ef9
child 20076 def4ad161528
     1.1 --- a/src/Pure/type_infer.ML	Fri May 05 21:59:44 2006 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Fri May 05 21:59:45 2006 +0200
     1.3 @@ -173,7 +173,8 @@
     1.4            (ps, PVar (xi, snd (pretyp_of (K true) ([], T))))
     1.5        | pre_of (ps, Var (xi, T)) = constrain (ps, PVar (xi, var_param xi)) T
     1.6        | pre_of (ps, Free (x, T)) = constrain (ps, PFree (x, var_param (x, ~1))) T
     1.7 -      | pre_of (ps, Const ("_type_constraint_", T) $ t) = constrain (pre_of (ps, t)) T
     1.8 +      | pre_of (ps, Const ("_type_constraint_", Type ("fun", [T, _])) $ t) =
     1.9 +          constrain (pre_of (ps, t)) T
    1.10        | pre_of (ps, Bound i) = (ps, PBound i)
    1.11        | pre_of (ps, Abs (x, T, t)) =
    1.12            let
    1.13 @@ -431,7 +432,7 @@
    1.14  
    1.15  fun constrain t T =
    1.16    if T = dummyT then t
    1.17 -  else Const ("_type_constraint_", T) $ t;
    1.18 +  else Const ("_type_constraint_", T --> T) $ t;
    1.19  
    1.20  
    1.21  (* user parameters *)