diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/Import/xml.ML
--- a/src/HOL/Import/xml.ML	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Import/xml.ML	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Import/xml.ML
-    ID:         $Id$
 
 Yet another version of XML support.
 *)
@@ -157,11 +156,11 @@
 
 fun tree_of_string s =
     let
-	val seq = Seq.fromString s
-	val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
-	val (x, toks) = scanner seq
+        val seq = Seq.fromString s
+        val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
+        val (x, toks) = scanner seq
     in
-	if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
+        if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
     end
 
 (* More efficient saving and loading of xml trees employing a proprietary external format *)
@@ -175,9 +174,9 @@
 fun write_tree (Text s) buf = buf |> Buffer.add "T" |> write_lstring s
   | write_tree (Elem (name, attrs, children)) buf = 
     buf |> Buffer.add "E" 
-	|> write_lstring name 
-	|> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs 
-	|> write_list write_tree children
+        |> write_lstring name 
+        |> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs 
+        |> write_list write_tree children
 
 fun parse_tree toks = (one (K true) :-- (fn "T" => parse_lstring >> Text | "E" => parse_elem | _ => raise SyntaxError) >> snd) toks
 and parse_elem toks = (parse_lstring -- parse_list (parse_lstring -- parse_lstring) -- parse_list parse_tree >> (fn ((n, a), c) => Elem (n,a,c))) toks
@@ -186,15 +185,15 @@
 
 fun tree_of_encoded_string s = 
     let
-	fun print (a,b) = writeln (a^" "^(string_of_int b))
-	val _ = print ("length of encoded string: ", size s)
-	val _ = writeln "Seq.fromString..."
-	val seq = timeit (fn () => Seq.fromString s)
-	val  _ = print ("length of sequence", timeit (fn () => Seq.length seq))
-	val scanner = !! (err "Malformed encoded xml") parse_tree
-	val (x, toks) = scanner seq
+        fun print (a,b) = writeln (a^" "^(string_of_int b))
+        val _ = print ("length of encoded string: ", size s)
+        val _ = writeln "Seq.fromString..."
+        val seq = timeit (fn () => Seq.fromString s)
+        val  _ = print ("length of sequence", timeit (fn () => Seq.length seq))
+        val scanner = !! (err "Malformed encoded xml") parse_tree
+        val (x, toks) = scanner seq
     in
-	if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
-    end	       
+        if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
+    end        
 
 end;