# HG changeset patch
# User blanchet
# Date 1391643837 -3600
# Node ID a593712f6878a4551160d11417563bde50125b2f
# Parent  5ebf832b58a15eebda94bed9fc5b9b3247b2425a
don't waste time with old-style 'case's that don't have the required theorems

diff -r 5ebf832b58a1 -r a593712f6878 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- 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