proper option, not catch-all pattern;

--- a/src/HOL/Tools/BNF/bnf_lift.ML	Mon Aug 31 22:28:23 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lift.ML	Mon Aug 31 22:30:41 2015 +0200
@@ -49,7 +49,7 @@
   let
     val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
       |> the_default Plugin_Name.default_filter;
-    val no_warn_wits = exists (can (fn Sequential_Option => ())) opts;
+    val no_warn_wits = exists (fn No_Warn_Wits => true | _ => false) opts;
 
     (* extract Rep Abs F RepT AbsT *)
     val (_, [Rep_G, Abs_G, F]) = Thm.prop_of thm