# HG changeset patch
# User blanchet
# Date 1447359129 -3600
# Node ID 61995131cf2818484c9ec599ea8adfc682495cc0
# Parent  ae5e55d03e455c344801ac42030a98dbe54d9c28
use cartouches instead of backquotes

diff -r ae5e55d03e45 -r 61995131cf28 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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}