# HG changeset patch
# User paulson
# Date 1287159697 -3600
# Node ID b253319c9a95ad87274fc93eb9782f59ff6ee86e
# Parent  c02078ff869181708608de625999aa6cca2518be# Parent  b654fa27fbc499fa406df1a50afe634b8e23084c
merged

diff -r c02078ff8691 -r b253319c9a95 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Oct 15 21:50:26 2010 +0900
+++ b/src/Pure/type.ML	Fri Oct 15 17:21:37 2010 +0100
@@ -418,10 +418,12 @@
 
 fun typ_match tsig =
   let
-    fun match (TVar (v, S), T) subs =
+    fun match (T0 as TVar (v, S), T) subs = 
           (case lookup subs (v, S) of
             NONE =>
-              if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
+              if of_sort tsig (T, S) 
+              then if T0 = T then subs (*types already identical; don't create cycle!*)
+                   else Vartab.update_new (v, (S, T)) subs
               else raise TYPE_MATCH
           | SOME U => if U = T then subs else raise TYPE_MATCH)
       | match (Type (a, Ts), Type (b, Us)) subs =
diff -r c02078ff8691 -r b253319c9a95 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Oct 15 21:50:26 2010 +0900
+++ b/src/Pure/unify.ML	Fri Oct 15 17:21:37 2010 +0100
@@ -205,6 +205,14 @@
 exception ASSIGN;  (*Raised if not an assignment*)
 
 
+fun self_asgt (ix,(_,TVar (ix',_))) = (ix = ix')
+  | self_asgt (ix, _) = false;
+
+fun check_tyenv msg tys tyenv = 
+  if Vartab.exists self_asgt tyenv
+  then raise TYPE (msg ^ ": looping type envir!!", tys, []) 
+  else tyenv;
+
 fun unify_types thy (T, U, env) =
   if T = U then env
   else
@@ -715,7 +723,7 @@
         fun result env =
           if Envir.above env maxidx then   (* FIXME proper handling of generated vars!? *)
             SOME (Envir.Envir {maxidx = maxidx,
-              tyenv = Vartab.make (map (norm_tvar env) pat_tvars),
+              tyenv = Vartab.make (filter_out self_asgt (map (norm_tvar env) pat_tvars)),
               tenv = Vartab.make (map (norm_var env) pat_vars)})
           else NONE;