--- 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]]