1.1 --- a/src/HOL/Tools/ctr_sugar.ML	Tue Nov 12 13:47:24 2013 +0100
     1.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 12 13:47:24 2013 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
     1.5    val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
     1.6    val ctr_sugars_of: Proof.context -> ctr_sugar list
     1.7 +  val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
     1.8    val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
     1.9    val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
    1.10  
    1.11 @@ -140,6 +141,9 @@
    1.12  fun ctr_sugars_of ctxt =
    1.13    Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
    1.14  
    1.15 +fun ctr_sugar_of_case ctxt s =
    1.16 +  find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);
    1.17 +
    1.18  fun register_ctr_sugar key ctr_sugar =
    1.19    Local_Theory.declaration {syntax = false, pervasive = true}
    1.20      (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));