--- 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 =
--- 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 "(" ")"
--- 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 []);
--- 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));