proper lemma [source] antiquotation
authorhaftmann
Mon May 26 17:55:37 2008 +0200 (2008-05-26)
changeset 26996090a619e7d87
parent 26995 2511a72dd73c
child 26997 40552bbac005
proper lemma [source] antiquotation
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 26 17:55:36 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 26 17:55:37 2008 +0200
     1.3 @@ -468,6 +468,8 @@
     1.4        |> Proof.global_terminal_proof (method_text, NONE);
     1.5    in pretty_term ctxt prop end;
     1.6  
     1.7 +val hd_src = Args.src o (apfst o apsnd) (single o hd) o Args.dest_src;
     1.8 +
     1.9  fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.10  
    1.11  fun pretty_term_style ctxt (name, t) =
    1.12 @@ -529,7 +531,7 @@
    1.13   [("thm", args Attrib.thms (output_list pretty_thm)),
    1.14    ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
    1.15    ("prop", args Args.prop (output pretty_term)),
    1.16 -  ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact)),
    1.17 +  ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact o hd_src)),
    1.18    ("term", args Args.term (output pretty_term)),
    1.19    ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
    1.20    ("term_type", args Args.term (output pretty_term_typ)),