# HG changeset patch
# User wenzelm
# Date 1148326021 -7200
# Node ID 26a268c299d86b171576885ceb492eacf67a815e
# Parent  7706aeac6cf12a7acb414ac7d0233fb75cbe39a6
export raw_unifys, could_unifys;

diff -r 7706aeac6cf1 -r 26a268c299d8 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat May 20 23:45:37 2006 +0200
+++ b/src/Pure/type.ML	Mon May 22 21:27:01 2006 +0200
@@ -60,7 +60,9 @@
   exception TUNIFY
   val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
   val raw_unify: typ * typ -> tyenv -> tyenv
+  val raw_unifys: typ list * typ list -> tyenv -> tyenv
   val could_unify: typ * typ -> bool
+  val could_unifys: typ list * typ list -> bool
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
@@ -437,7 +439,8 @@
       else raw_unifys (Ts, Us) tye
   | (T, U) => if T = U then tye else raise TUNIFY)
 and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)
-  | raw_unifys _ tye = tye;
+  | raw_unifys ([], []) tye = tye
+  | raw_unifys _ _ = raise TUNIFY;
 
 (*fast unification filter*)
 fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us)
@@ -446,7 +449,8 @@
   | could_unify (_, TVar _) = true
   | could_unify _ = false
 and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us)
-  | could_unifys _ = true;
+  | could_unifys ([], []) = true
+  | could_unifys _ = false;
 
 
 (*equality with respect to a type environment*)