assign now applies meet before update_new to avoid misleading error message.
--- 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 *)