--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Nov 12 13:50:54 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Nov 12 21:12:09 2015 +0100
@@ -81,7 +81,7 @@
| explode_interval max (Facts.From i) = i upto i + max - 1
| explode_interval _ (Facts.Single i) = [i]
-val backquote = raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
+val backquote = enclose "\<open>" "\<close>"
(* unfolding these can yield really huge terms *)
val risky_defs = @{thms Bit0_def Bit1_def}