fail with low-level exception, not user error;

--- 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.