diff -r 792f3cf59d95 -r d6f7418ea9dd src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Feb 03 15:28:01 2014 +0100
+++ b/src/Tools/subtyping.ML	Mon Feb 03 15:31:47 2014 +0100
@@ -140,7 +140,7 @@
   (case (T, Type_Infer.deref tye U) of
     (TVar (xi, _), U) => [(xi, U)]
   | (Type (a, Ts), Type (b, Us)) =>
-      if a <> b then raise error (eval_err err) else inst_collects tye err Ts Us
+      if a <> b then error (eval_err err) else inst_collects tye err Ts Us
   | (_, U') => if T <> U' then error (eval_err err) else [])
 and inst_collects tye err Ts Us =
   fold2 (fn T => fn U => fn is => inst_collect tye err T U @ is) Ts Us [];