src/Pure/Isar/isar_output.ML

   if ! display then s else Symbol.strip_blanks s;
 
 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
 
 fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term_abbrev ctxt =
+  ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
 
 fun pretty_term_typ ctxt t =
   ProofContext.pretty_term ctxt (TypeInfer.constrain t (Term.fastype_of t));
 
 fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
 
 fun pretty_term_const ctxt t =
   if Term.is_Const t then pretty_term ctxt t
   else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
+
+fun pretty_abbrev ctxt t =
+  let
+    fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
+    val (head, args) = Term.strip_comb t;
+    val (c, T) = Term.dest_Const head handle TERM _ => err ();
+    val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
+      handle TYPE _ => err ();
+    val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
+  in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 fun pretty_term_style ctxt (name, t) =
   pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t);

   ("term", args Args.term (output pretty_term)),
   ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
   ("term_type", args Args.term (output pretty_term_typ)),
   ("typeof", args Args.term (output pretty_term_typeof)),
   ("const", args Args.term (output pretty_term_const)),
+  ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
   ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output (K pretty_text))),
   ("goals", output_goals true),
   ("subgoals", output_goals false),
   ("prf", args Attrib.thms (output (pretty_prf false))),