diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/TPTP/MaSh_Export_Base.thy
--- a/src/HOL/TPTP/MaSh_Export_Base.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
 *)
 
-section {* MaSh Exporter Base *}
+section \<open>MaSh Exporter Base\<close>
 
 theory MaSh_Export_Base
 imports Main
@@ -19,15 +19,15 @@
 
 hide_fact (open) HOL.ext
 
-ML {*
+ML \<open>
 Multithreading.max_threads ()
-*}
+\<close>
 
-ML {*
+ML \<open>
 open MaSh_Export
-*}
+\<close>
 
-ML {*
+ML \<open>
 val do_it = false (* switch to "true" to generate the files *)
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
@@ -37,6 +37,6 @@
 val max_suggestions = 1024
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
-*}
+\<close>
 
 end