declaration attribute for case combinators

--- a/src/HOL/Tools/case_translation.ML	Tue Apr 09 18:27:49 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 17:49:16 2013 +0200
@@ -569,7 +569,11 @@
   trfun_setup #>
   trfun_setup' #>
   term_check_setup #>
-  term_uncheck_setup;
+  term_uncheck_setup #>
+  Attrib.setup @{binding case_translation}
+    (Args.term -- Scan.repeat1 Args.term >>
+      (fn (t, ts) => Thm.declaration_attribute (K (register t ts))))
+    "declaration of case combinators and constructors";
 
 
 (* outer syntax commands *)