# HG changeset patch
# User blanchet
# Date 1292761518 -3600
# Node ID e0400b05a62c947cc4422f4c970cb7d53c6a74a8
# Parent  8e1cde88aae6f3db7e8a17e02d3828301af1d90e
escape backticks in altstrings

diff -r 8e1cde88aae6 -r e0400b05a62c src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun Dec 19 11:48:42 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sun Dec 19 13:25:18 2010 +0100
@@ -101,6 +101,8 @@
   | 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 "`" "`"
 fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
   let
     val ths = Attrib.eval_thms ctxt [xthm]
@@ -109,7 +111,7 @@
                                ^ "]") args)
     fun nth_name j =
       case xref of
-        Facts.Fact s => "`" ^ s ^ "`" ^ bracket
+        Facts.Fact s => backquote s ^ bracket
       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
       | Facts.Named ((name, _), NONE) =>
         make_name reserved (length ths > 1) (j + 1) name ^ bracket
@@ -804,8 +806,8 @@
         else
           let
             val multi = length ths > 1
-            val backquotify =
-              enclose "`" "`" o string_for_term ctxt o close_form o prop_of
+            val backquote_thm =
+              backquote o string_for_term ctxt o close_form o prop_of
             fun check_thms a =
               case try (ProofContext.get_thms ctxt) a of
                 NONE => false
@@ -820,7 +822,7 @@
                   else
                     (((fn () =>
                           if name0 = "" then
-                            th |> backquotify
+                            th |> backquote_thm
                           else
                             let
                               val name1 = Facts.extern facts name0