src/Pure/General/pretty.ML

   val brk: int -> T
   val fbrk: T
   val blk: int * T list -> T
   val unbreakable: T -> T
   val quote: T -> T
+  val backquote: T -> T
   val commas: T list -> T list
   val breaks: T list -> T list
   val fbreaks: T list -> T list
   val block: T list -> T
   val strs: string list -> T

   | unbreakable (e as String _) = e;
 
 
 (* utils *)
 
-fun quote prt =
-  blk (1, [str "\"", prt, str "\""]);
+fun quote prt = blk (1, [str "\"", prt, str "\""]);
+fun backquote prt = blk (1, [str "`", prt, str "`"]);
 
 fun separate_pretty sep prts =
   prts
   |> map single
   |> separate [str sep, brk 1]