author | traytel |
Wed, 10 Apr 2013 17:49:16 +0200 | |
changeset 51681 | bdfa3b947992 |
parent 51680 | 8b8cd5a527bc |
child 51682 | bdaa1582dc8b |
--- 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 *)