1.1 --- a/src/Pure/ML/ml_thms.ML	Tue Dec 21 19:35:36 2010 +0100
     1.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Dec 21 21:05:50 2010 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4        val i = serial ();
     1.5        val (a, background') = background
     1.6          |> ML_Antiquote.variant kind ||> put_thms (i, ths);
     1.7 -      val ml = (thm_bind kind a i, "Isabelle." ^ a);
     1.8 +      val ml = (thm_bind kind a i, " Isabelle." ^ a ^ " ");
     1.9      in (K ml, background') end));
    1.10  
    1.11  val _ = thm_antiq "thm" (Attrib.thm >> single);
    1.12 @@ -69,7 +69,8 @@
    1.13          val (a, background') = background
    1.14            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
    1.15          val ml =
    1.16 -          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
    1.17 +          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i,
    1.18 +            " Isabelle." ^ a ^ " ");
    1.19        in (K ml, background') end));
    1.20  
    1.21  end;