diff -r eff000cab70f -r 893b15200ec1 src/HOL/List.thy
--- 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};