src/HOL/Tools/TFL/tfl.ML

 fun alpha_ex_unroll (xlist, tm) =
   let val (qvars,body) = USyntax.strip_exists tm
       val vlist = #2 (USyntax.strip_comb (USyntax.rhs body))
       val plist = ListPair.zip (vlist, xlist)
       val args = map (the o AList.lookup (op aconv) plist) qvars
-                   handle Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
+                   handle Option.Option => raise Fail "TFL.alpha_ex_unroll: no correspondence"
       fun build ex      []   = []
         | build (_$rex) (v::rst) =
            let val ex1 = Term.betapply(rex, v)
            in  ex1 :: build ex1 rst
            end