diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu May 26 17:51:22 2016 +0200
@@ -1,7 +1,7 @@
 
 (* Author: Ondrej Kuncar, TU Muenchen *)
 
-section {* Pervasive test of code generator *}
+section \<open>Pervasive test of code generator\<close>
 
 theory Generate_Efficient_Datastructures
 imports
@@ -18,7 +18,7 @@
   val consts = map_filter (try (curry (Axclass.param_of_inst thy)
     @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
 in fold Code.del_eqns consts thy end
-\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
+\<close> \<comment> \<open>drop technical stuff from \<open>Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
 
 (* 
    The following code equations have to be deleted because they use