assign now applies meet before update_new to avoid misleading error message.
authorberghofe
Tue, 01 Jun 2010 11:16:16 +0200
changeset 37235cafcc42bae77
parent 37234 95bfc649fe19
child 37236 739d8b9c59da
assign now applies meet before update_new to avoid misleading error message.
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Tue Jun 01 11:13:40 2010 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Jun 01 11:16:16 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 *)