src/HOL/List.thy
changeset 52143 36ffe23b25f8
parent 52131 366fa32ee2a3
child 52148 893b15200ec1
--- a/src/HOL/List.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/List.thy	Sat May 25 15:37:53 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};