assign now applies meet before update_new to avoid misleading error message.
authorberghofe
Tue, 01 Jun 2010 11:16:16 +0200
changeset 37235 cafcc42bae77
parent 37234 95bfc649fe19
child 37236 739d8b9c59da
assign now applies meet before update_new to avoid misleading error message.
src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Tue Jun 01 11:13:40 2010 +0200
+++ b/src/Pure/type_infer.ML	Tue Jun 01 11:16:16 2010 +0200
@@ -295,11 +295,11 @@
       | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts
       | occurs_check _ _ _ = ();
 
-    fun assign i (T as Param (i', _)) S (tye_idx as (tye, idx)) =
+    fun assign i (T as Param (i', _)) S tye_idx =
           if i = i' then tye_idx
-          else meet (T, S) (Inttab.update_new (i, T) tye, idx)
-      | assign i T S (tye, idx) =
-          (occurs_check tye i T; meet (T, S) (Inttab.update_new (i, T) tye, idx));
+          else tye_idx |> meet (T, S) |>> Inttab.update_new (i, T)
+      | assign i T S (tye_idx as (tye, _)) =
+          (occurs_check tye i T; tye_idx |> meet (T, S) |>> Inttab.update_new (i, T));
 
 
     (* unification *)