1.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Nov 03 10:20:37 2010 +0100
     1.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Nov 03 10:48:55 2010 +0100
     1.3 @@ -607,8 +607,7 @@
     1.4        val vlist = #2(S.strip_comb (S.rhs body))
     1.5        val plist = ListPair.zip (vlist, xlist)
     1.6        val args = map (the o AList.lookup (op aconv) plist) qvars
     1.7 -                   handle Option => sys_error
     1.8 -                       "TFL fault [alpha_ex_unroll]: no correspondence"
     1.9 +                   handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
    1.10        fun build ex      []   = []
    1.11          | build (_$rex) (v::rst) =
    1.12             let val ex1 = Term.betapply(rex, v)