# HG changeset patch
# User wenzelm
# Date 1294605221 -3600
# Node ID 82c1e348bc18ee92ef5be2936c33e981904bd284
# Parent  6c0de045d127c5609eada6026854a59b75cee051
reverted 08240feb69c7 -- breaks positions of reports;

diff -r 6c0de045d127 -r 82c1e348bc18 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sun Jan 09 19:58:08 2011 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sun Jan 09 21:33:41 2011 +0100
@@ -48,7 +48,7 @@
     let
       val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
       val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
-      val body = " Isabelle." ^ a ^ " ";
+      val body = "Isabelle." ^ a;
     in (K (env, body), background') end));
 
 val value = declaration "val";
diff -r 6c0de045d127 -r 82c1e348bc18 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Jan 09 19:58:08 2011 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sun Jan 09 21:33:41 2011 +0100
@@ -39,7 +39,7 @@
       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);
@@ -69,8 +69,7 @@
         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;
diff -r 6c0de045d127 -r 82c1e348bc18 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sun Jan 09 19:58:08 2011 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sun Jan 09 21:33:41 2011 +0100
@@ -234,7 +234,7 @@
     val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
     val (ml_code, consts_map) = Lazy.force acc_code;
     val ml_code = if is_first then ml_code else "";
-    val body = " Isabelle." ^ the (AList.lookup (op =) consts_map const) ^ " ";
+    val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const);
   in (ml_code, body) end;
 
 in