# HG changeset patch
# User traytel
# Date 1365608956 -7200
# Node ID bdfa3b947992a894e5dde70e6778d23e0c5aaf37
# Parent  8b8cd5a527bcaa88167e91d6e6b9809d6142c596
declaration attribute for case combinators

diff -r 8b8cd5a527bc -r bdfa3b947992 src/HOL/Tools/case_translation.ML
--- 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 *)