src/Pure/ML/ml_thms.ML

   (fn _ => scan >> (fn ths => fn background =>
     let
       val i = serial ();
       val (a, background') = background
         |> ML_Antiquote.variant kind ||> put_thms (i, ths);
-      val ml = (thm_bind kind a i, "Isabelle." ^ a);
+      val ml = (thm_bind kind a i, " Isabelle." ^ a ^ " ");
     in (K ml, background') end));
 
 val _ = thm_antiq "thm" (Attrib.thm >> single);
 val _ = thm_antiq "thms" Attrib.thms;
 

           |> Proof.theorem NONE after_qed propss
           |> Proof.global_terminal_proof methods;
         val (a, background') = background
           |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
         val ml =
-          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
+          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i,
+            " Isabelle." ^ a ^ " ");
       in (K ml, background') end));
 
 end;