# HG changeset patch
# User wenzelm
# Date 1452179413 -3600
# Node ID 7d47cf67516de3215437d62caa6e4b2710ebef4b
# Parent  bd73a2279fcdc002e07463296a6995b510c2901c
prefer non-ASCII output;

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 =
diff -r bd73a2279fcd -r 7d47cf67516d src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Thu Jan 07 15:53:39 2016 +0100
+++ b/src/Pure/Isar/bundle.ML	Thu Jan 07 16:10:13 2016 +0100
@@ -124,7 +124,7 @@
 
 fun print_bundles verbose ctxt =
   let
-    val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
+    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
 
     fun prt_fact (ths, []) = map prt_thm ths
       | prt_fact (ths, atts) = Pretty.enclose "(" ")"
diff -r bd73a2279fcd -r 7d47cf67516d src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Jan 07 15:53:39 2016 +0100
+++ b/src/Pure/Isar/element.ML	Thu Jan 07 16:10:13 2016 +0100
@@ -152,7 +152,7 @@
   let
     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
-    val prt_thm = Pretty.backquote o Thm.pretty_thm ctxt;
+    val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
 
     fun prt_binding (b, atts) =
       Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
diff -r bd73a2279fcd -r 7d47cf67516d src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Jan 07 15:53:39 2016 +0100
+++ b/src/Pure/Isar/token.ML	Thu Jan 07 16:10:13 2016 +0100
@@ -471,7 +471,7 @@
   | SOME (Typ T) => Syntax.pretty_typ ctxt T
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
-      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Thm.pretty_thm ctxt) ths))
+      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.cartouche o Thm.pretty_thm ctxt) ths))
   | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));