changeset 52148 | 893b15200ec1 |
parent 52141 | eff000cab70f |
parent 52143 | 36ffe23b25f8 |
child 52379 | 7f864f2219a9 |
--- a/src/HOL/List.thy Sat May 25 15:44:29 2013 +0200 +++ b/src/HOL/List.thy Sat May 25 18:30:38 2013 +0200 @@ -386,7 +386,7 @@ syntax (HTML output) "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _") -parse_translation (advanced) {* +parse_translation {* let val NilC = Syntax.const @{const_syntax Nil}; val ConsC = Syntax.const @{const_syntax Cons};