# HG changeset patch
# User wenzelm
# Date 1441053041 -7200
# Node ID f9be8241317032ccc81fb4bdcc3b5909b51d24c4
# Parent  c6ac3c3fbb85c322088aa6790d997c718e8e997f
proper option, not catch-all pattern;

diff -r c6ac3c3fbb85 -r f9be82413170 src/HOL/Tools/BNF/bnf_lift.ML
--- 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