src/HOL/List.thy
changeset 52143 36ffe23b25f8
parent 52131 366fa32ee2a3
child 52148 893b15200ec1
     1.1 --- a/src/HOL/List.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/List.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -386,7 +386,7 @@
     1.4  syntax (HTML output)
     1.5    "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
     1.6  
     1.7 -parse_translation (advanced) {*
     1.8 +parse_translation {*
     1.9    let
    1.10      val NilC = Syntax.const @{const_syntax Nil};
    1.11      val ConsC = Syntax.const @{const_syntax Cons};