changeset 37637 | ade245a81481 |
parent 37636 | ab50854da897 |
child 37720 | 50a9e2fa4f6b |
--- 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.