# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID 6401e2d5e68f3f9ce916cf489cc0912016b18db5
# Parent  d229f9749507f01cdcab91248727d8a3d7ac6eca
reused code

diff -r d229f9749507 -r 6401e2d5e68f src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -305,12 +305,6 @@
   register_coinduct_dynamic_base fpT_name
   #> ensure_codatatype_extra fpT_name;
 
-(*TODO: Merge with primcorec "case_of"*)
-fun case_of ctxt fcT_name =
-  (case ctr_sugar_of ctxt fcT_name of
-    SOME {casex = Const (s, _), ...} => SOME s
-  | _ => NONE);
-
 fun is_set ctxt (const_name, T) =
   (case T of
     Type (@{type_name fun}, [Type (fpT_name, _), Type (@{type_name set}, [_])]) =>
@@ -1476,7 +1470,7 @@
             if n < length args then
               (case gen_body_fun_T of
                 Type (_, [Type (T_name, _), _]) =>
-                if case_of lthy T_name = SOME c then
+                if case_of lthy T_name = SOME (c, true) then
                   let
                     val brancheTs = binder_fun_types (fastype_of1 (bound_Ts, casex));
                     val obj_leftover_Ts = map (curry fastype_of1 bound_Ts) obj_leftovers;