# HG changeset patch
# User blanchet
# Date 1384260444 -3600
# Node ID 40382f65bc80e4de5d547d4947b3fcce26e28024
# Parent  5d1b7ee6070e958a0bd538c3ec0833377d58d57c
added convenience function

diff -r 5d1b7ee6070e -r 40382f65bc80 src/HOL/Tools/ctr_sugar.ML
--- a/src/HOL/Tools/ctr_sugar.ML	Tue Nov 12 13:47:24 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Tue Nov 12 13:47:24 2013 +0100
@@ -36,6 +36,7 @@
   val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
   val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
   val ctr_sugars_of: Proof.context -> ctr_sugar list
+  val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
   val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
   val register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
 
@@ -140,6 +141,9 @@
 fun ctr_sugars_of ctxt =
   Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
 
+fun ctr_sugar_of_case ctxt s =
+  find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);
+
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));