src/Pure/type.ML
changeset 19696 26a268c299d8
parent 19694 08894a78400b
child 19806 f860b7a98445
     1.1 --- a/src/Pure/type.ML	Sat May 20 23:45:37 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Mon May 22 21:27:01 2006 +0200
     1.3 @@ -60,7 +60,9 @@
     1.4    exception TUNIFY
     1.5    val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
     1.6    val raw_unify: typ * typ -> tyenv -> tyenv
     1.7 +  val raw_unifys: typ list * typ list -> tyenv -> tyenv
     1.8    val could_unify: typ * typ -> bool
     1.9 +  val could_unifys: typ list * typ list -> bool
    1.10    val eq_type: tyenv -> typ * typ -> bool
    1.11  
    1.12    (*extend and merge type signatures*)
    1.13 @@ -437,7 +439,8 @@
    1.14        else raw_unifys (Ts, Us) tye
    1.15    | (T, U) => if T = U then tye else raise TUNIFY)
    1.16  and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)
    1.17 -  | raw_unifys _ tye = tye;
    1.18 +  | raw_unifys ([], []) tye = tye
    1.19 +  | raw_unifys _ _ = raise TUNIFY;
    1.20  
    1.21  (*fast unification filter*)
    1.22  fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us)
    1.23 @@ -446,7 +449,8 @@
    1.24    | could_unify (_, TVar _) = true
    1.25    | could_unify _ = false
    1.26  and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us)
    1.27 -  | could_unifys _ = true;
    1.28 +  | could_unifys ([], []) = true
    1.29 +  | could_unifys _ = false;
    1.30  
    1.31  
    1.32  (*equality with respect to a type environment*)