# HG changeset patch
# User wenzelm
# Date 1293743238 -3600
# Node ID 2db1d3d2ed54cd7ae9f878e1a52cc20e9aa1458e
# Parent  005e7f8d02a7b078b24387043bb126bb0041127a
uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);

diff -r 005e7f8d02a7 -r 2db1d3d2ed54 src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Dec 30 13:31:32 2010 +0100
+++ b/src/Pure/type.ML	Thu Dec 30 22:07:18 2010 +0100
@@ -418,12 +418,11 @@
 
 fun typ_match tsig =
   let
-    fun match (T0 as TVar (v, S), T) subs =
+    fun match (V as TVar (v, S), T) subs =
           (case lookup subs (v, S) of
             NONE =>
-              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
+              if V = T then subs
+              else if of_sort tsig (T, S) then 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 =
@@ -440,9 +439,9 @@
   (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
 
 (*purely structural matching*)
-fun raw_match (TVar (v, S), T) subs =
+fun raw_match (V as TVar (v, S), T) subs =
       (case lookup subs (v, S) of
-        NONE => Vartab.update_new (v, (S, T)) subs
+        NONE => if V = T then subs else Vartab.update_new (v, (S, T)) subs
       | SOME U => if U = T then subs else raise TYPE_MATCH)
   | raw_match (Type (a, Ts), Type (b, Us)) subs =
       if a <> b then raise TYPE_MATCH