diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/TPTP/ATP_Problem_Import.thy
--- a/src/HOL/TPTP/ATP_Problem_Import.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
 *)
 
-section {* ATP Problem Importer *}
+section \<open>ATP Problem Importer\<close>
 
 theory ATP_Problem_Import
 imports Complex_Main TPTP_Interpret "~~/src/HOL/Library/Refute"
@@ -10,7 +10,7 @@
 
 ML_file "sledgehammer_tactics.ML"
 
-ML {* Proofterm.proofs := 0 *}
+ML \<open>Proofterm.proofs := 0\<close>
 
 declare [[show_consts]] (* for Refute *)
 declare [[smt_oracle]]