1.1 --- a/src/Pure/Thy/thy_output.ML Tue Apr 29 15:25:50 2008 +0200
1.2 +++ b/src/Pure/Thy/thy_output.ML Tue Apr 29 19:55:02 2008 +0200
1.3 @@ -456,6 +456,13 @@
1.4 val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
1.5 in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
1.6
1.7 +fun pretty_fact ctxt (prop, method_text) =
1.8 + let
1.9 + val _ = ctxt
1.10 + |> Proof.theorem_i NONE (K I) [[(prop, [])]]
1.11 + |> Proof.global_terminal_proof (method_text, NONE);
1.12 + in pretty_term ctxt prop end;
1.13 +
1.14 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
1.15
1.16 fun pretty_term_style ctxt (name, t) =
1.17 @@ -517,6 +524,7 @@
1.18 [("thm", args Attrib.thms (output_list pretty_thm)),
1.19 ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
1.20 ("prop", args Args.prop (output pretty_term)),
1.21 + ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact)),
1.22 ("term", args Args.term (output pretty_term)),
1.23 ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
1.24 ("term_type", args Args.term (output pretty_term_typ)),