removed remains of Oheimb's double-space (cf. 0a5af667dc75);

--- a/src/Pure/General/symbol.ML	Mon Nov 26 19:53:43 2012 +0100
+++ b/src/Pure/General/symbol.ML	Mon Nov 26 19:56:09 2012 +0100
@@ -370,8 +370,7 @@
     ("\\<Psi>", Letter),
     ("\\<Omega>", Letter),
     ("\\<^isub>", Letter),
-    ("\\<^isup>", Letter),
-    ("\\<spacespace>", Blank)];
+    ("\\<^isup>", Letter)];
 in
   fun kind s =
     if is_ascii_letter s then Letter
@@ -536,7 +535,6 @@
   if not (is_printable s) then (0: int)
   else if String.isPrefix "\\<long" s then 2
   else if String.isPrefix "\\<Long" s then 2
-  else if s = "\\<spacespace>" then 2
   else 1;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;

--- a/src/Pure/General/symbol.scala	Mon Nov 26 19:53:43 2012 +0100
+++ b/src/Pure/General/symbol.scala	Mon Nov 26 19:56:09 2012 +0100
@@ -346,8 +346,7 @@
 
       "\\<^isub>", "\\<^isup>")
 
-    val blanks =
-      recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
+    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")

--- a/src/Pure/Thy/html.ML	Mon Nov 26 19:53:43 2012 +0100
+++ b/src/Pure/Thy/html.ML	Mon Nov 26 19:56:09 2012 +0100
@@ -61,7 +61,6 @@
    [("", (0, "")),
     ("\n", (0, "<br/>")),
     ("'", (1, "&#39;")),
-    ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
     ("\\<exclamdown>", (1, "&iexcl;")),
     ("\\<cent>", (1, "&cent;")),
     ("\\<pounds>", (1, "&pound;")),

--- a/src/Tools/WWW_Find/html_unicode.ML	Mon Nov 26 19:53:43 2012 +0100
+++ b/src/Tools/WWW_Find/html_unicode.ML	Mon Nov 26 19:56:09 2012 +0100
@@ -25,8 +25,7 @@
 
 local
   val sym_width_lookup = Symtab.make
-   [("\<spacespace>", 2),
-    ("\<Longleftarrow>", 2),
+   [("\<Longleftarrow>", 2),
     ("\<longleftarrow>", 2),
     ("\<Longrightarrow>", 2),
     ("\<longrightarrow>", 2),

--- a/src/Tools/WWW_Find/www/find_theorems.js	Mon Nov 26 19:53:43 2012 +0100
+++ b/src/Tools/WWW_Find/www/find_theorems.js	Mon Nov 26 19:56:09 2012 +0100
@@ -26,7 +26,6 @@
 utf8['\\<FF>'] = '𝔉';
 utf8['\\<II>'] = 'ℑ';
 utf8['\\<VV>'] = '𝔙';
-utf8['\\<spacespace>'] = '␣';
 utf8['\\<and>'] = '∧';
 utf8['\\<mapsto>'] = '↦';
 utf8['\\<ll>'] = '𝔩';