don't waste time with old-style 'case's that don't have the required theorems

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Feb 06 00:24:02 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Feb 06 00:43:57 2014 +0100
@@ -344,7 +344,8 @@
   let
     fun ctr_sugar_of_case c s =
       (case ctr_sugar_of ctxt s of
-        SOME (ctr_sugar as {casex = Const (c', _), ...}) => if c' = c then SOME ctr_sugar else NONE
+        SOME (ctr_sugar as {casex = Const (c', _), sel_splits = _ :: _, ...}) =>
+        if c' = c then SOME ctr_sugar else NONE
       | _ => NONE);
     fun add_ctr_sugar (s, Type (@{type_name fun}, [_, T])) =
         binder_types T