--- 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) ->