diff -r bd73a2279fcd -r 7d47cf67516d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Jan 07 15:53:39 2016 +0100
+++ b/src/Pure/General/pretty.ML	Thu Jan 07 16:10:13 2016 +0100
@@ -45,7 +45,6 @@
   val paragraph: T list -> T
   val para: string -> T
   val quote: T -> T
-  val backquote: T -> T
   val cartouche: T -> T
   val separate: string -> T list -> T list
   val commas: T list -> T list
@@ -168,7 +167,6 @@
 val para = paragraph o text;
 
 fun quote prt = blk (1, [str "\"", prt, str "\""]);
-fun backquote prt = blk (1, [str "`", prt, str "`"]);
 fun cartouche prt = blk (1, [str "\\<open>", prt, str "\\<close>"]);
 
 fun separate sep prts =