uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
authorwenzelm
Thu Dec 30 22:07:18 2010 +0100 (2010-12-30)
changeset 414212db1d3d2ed54
parent 41420 005e7f8d02a7
child 41422 8a765db7e0f8
uniform treatment of typ_match and raw_match (cf. b654fa27fbc4);
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Thu Dec 30 13:31:32 2010 +0100
     1.2 +++ b/src/Pure/type.ML	Thu Dec 30 22:07:18 2010 +0100
     1.3 @@ -418,12 +418,11 @@
     1.4  
     1.5  fun typ_match tsig =
     1.6    let
     1.7 -    fun match (T0 as TVar (v, S), T) subs =
     1.8 +    fun match (V as TVar (v, S), T) subs =
     1.9            (case lookup subs (v, S) of
    1.10              NONE =>
    1.11 -              if of_sort tsig (T, S)
    1.12 -              then if T0 = T then subs (*types already identical; don't create cycle!*)
    1.13 -                   else Vartab.update_new (v, (S, T)) subs
    1.14 +              if V = T then subs
    1.15 +              else if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
    1.16                else raise TYPE_MATCH
    1.17            | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.18        | match (Type (a, Ts), Type (b, Us)) subs =
    1.19 @@ -440,9 +439,9 @@
    1.20    (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
    1.21  
    1.22  (*purely structural matching*)
    1.23 -fun raw_match (TVar (v, S), T) subs =
    1.24 +fun raw_match (V as TVar (v, S), T) subs =
    1.25        (case lookup subs (v, S) of
    1.26 -        NONE => Vartab.update_new (v, (S, T)) subs
    1.27 +        NONE => if V = T then subs else Vartab.update_new (v, (S, T)) subs
    1.28        | SOME U => if U = T then subs else raise TYPE_MATCH)
    1.29    | raw_match (Type (a, Ts), Type (b, Us)) subs =
    1.30        if a <> b then raise TYPE_MATCH