diff -r ca505e7b7591 -r 19ae7064f00f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Jun 28 15:30:46 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Jun 28 21:21:13 2008 +0200
@@ -463,15 +463,13 @@
     val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
   in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;
 
-fun pretty_fact ctxt (prop, method_text) =
+fun pretty_lemma ctxt (prop, method_text) =
   let
     val _ = ctxt
       |> Proof.theorem_i NONE (K I) [[(prop, [])]]
       |> Proof.global_terminal_proof (method_text, NONE);
   in pretty_term ctxt prop end;
 
-val hd_src = Args.src o (apfst o apsnd) (single o hd) o Args.dest_src;
-
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 fun pretty_term_style ctxt (name, t) =
@@ -529,11 +527,17 @@
 
 (* commands *)
 
+val embedded_lemma =
+  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args))
+    (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
+
+val _ = OuterKeyword.keyword "by";
+
 val _ = add_commands
  [("thm", args Attrib.thms (output_list pretty_thm)),
   ("thm_style", args (Scan.lift Args.liberal_name -- Attrib.thm) (output pretty_thm_style)),
   ("prop", args Args.prop (output pretty_term)),
-  ("lemma", args (Args.prop -- Scan.lift Method.simple_text) (output pretty_fact o hd_src)),
+  ("lemma", embedded_lemma),
   ("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)),