# HG changeset patch
# User wenzelm
# Date 1277845169 -7200
# Node ID ade245a81481b587ca3a2249f24befcce145f599
# Parent  ab50854da8970c9fba0619622503cce74fbbf028
fail with low-level exception, not user error;

diff -r ab50854da897 -r ade245a81481 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Tue Jun 29 21:56:31 2010 +0200
+++ b/src/Pure/unify.ML	Tue Jun 29 22:59:29 2010 +0200
@@ -457,7 +457,7 @@
 (*Form the arguments into records for deletion/sorting.*)
 fun flexargs ([], [], []) = [] : flarg list
   | flexargs (j :: js, t :: ts, T :: Ts) = {j = j, t = t, T = T} :: flexargs (js, ts, Ts)
-  | flexargs _ = error "flexargs";
+  | flexargs _ = raise Fail "flexargs";
 
 
 (*If an argument contains a banned Bound, then it should be deleted.