diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Thu May 26 17:51:22 2016 +0200
@@ -42,19 +42,19 @@
 
 end
 
-ML {* 
+ML \<open>
 val small_15_active = Attrib.setup_config_bool @{binding quickcheck_small_14_active} (K false);
 val small_14_active = Attrib.setup_config_bool @{binding quickcheck_small_15_active} (K false);
-*}
+\<close>
 
-setup {*
+setup \<open>
   Context.theory_map (Quickcheck.add_tester ("small_generators_depth_14",
     (small_14_active, Predicate_Compile_Quickcheck.test_goals
       (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 14))))
   #> Context.theory_map (Quickcheck.add_tester ("small_generators_depth_15",
     (small_15_active, Predicate_Compile_Quickcheck.test_goals
       (Predicate_Compile_Aux.Pos_Generator_DSeq, true, true, 15))))
-*}
+\<close>
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"