# HG changeset patch
# User wenzelm
# Date 1391437907 -3600
# Node ID d6f7418ea9dd69a7cc24cd3a941e6ebcfb8b06fa
# Parent  792f3cf59d951f7f74b6c527741bdf5c89ad736f
just error, not a failed attempt to raise an exception;

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 [];