src/Pure/type_infer.ML
changeset 37236 739d8b9c59da
parent 37153 01aa36932739
parent 37235 cafcc42bae77
child 39539 1f8131a7bcb9
     1.1 --- a/src/Pure/type_infer.ML	Tue Jun 01 11:18:51 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Jun 01 11:30:57 2010 +0200
     1.3 @@ -295,11 +295,11 @@
     1.4        | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
     1.5        | occurs_check _ _ _ = ();
     1.6  
     1.7 -    fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) =
     1.8 +    fun assign i (T as Param (i', _)) S tye_idx =
     1.9            if i = i' then tye_idx
    1.10 -          else meet (T, S) (Inttab.update_new (i, T) tye, idx)
    1.11 -      | assign i T S (tye, idx) =
    1.12 -          (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx));
    1.13 +          else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
    1.14 +      | assign i T S (tye_idx as (tye, _)) =
    1.15 +          (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
    1.16  
    1.17  
    1.18      (* unification *)