diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Mirabelle/Mirabelle_Test.thy
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
     Author:     Sascha Boehme, TU Munich
 *)
 
-section {* Simple test theory for Mirabelle actions *}
+section \<open>Simple test theory for Mirabelle actions\<close>
 
 theory Mirabelle_Test
 imports Main Mirabelle
@@ -16,9 +16,9 @@
 ML_file "Tools/mirabelle_sledgehammer_filter.ML"
 ML_file "Tools/mirabelle_try0.ML"
 
-text {*
+text \<open>
   Only perform type-checking of the actions,
   any reasonable test would be too complicated.
-*}
+\<close>
 
 end