src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 61646 61995131cf28
parent 61322 44f4ffe2b210
child 61877 276ad4354069
--- 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}