--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 04 23:22:53 2019 +0100
@@ -40,7 +40,7 @@
open Sledgehammer_Proof_Methods
open Sledgehammer_Isar_Proof
-val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
+val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_preplay_trace\<close> (K false)
fun peek_at_outcome outcome =
if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime