--- a/src/Pure/Isar/isar_output.ML Sat Dec 09 18:05:34 2006 +0100
+++ b/src/Pure/Isar/isar_output.ML Sat Dec 09 18:05:36 2006 +0100
@@ -441,6 +441,8 @@
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));
@@ -451,6 +453,16 @@
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) =
@@ -517,6 +529,7 @@
("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),