# HG changeset patch
# User blanchet
# Date 1458629822 -3600
# Node ID 6e8924f957f6838ce9ae47fbb5bb0f460dd9925e
# Parent  1e5cf471e7030c25340d7487a35d5bd33365c151
export ML function

diff -r 1e5cf471e703 -r 6e8924f957f6 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 22 07:57:01 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 22 07:57:02 2016 +0100
@@ -57,6 +57,7 @@
   val s_disjs: term list -> term
   val s_dnf: term list list -> term list
 
+  val case_of: Proof.context -> string -> (string * bool) option
   val fold_rev_let_if_case: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list ->
     term -> 'a -> 'a
   val massage_let_if_case: Proof.context -> (term -> bool) -> (typ list -> term -> term) ->