total Symbol.source;

--- a/src/HOL/Import/import_syntax.ML	Sat Nov 13 19:47:23 2010 +0100
+++ b/src/HOL/Import/import_syntax.ML	Sat Nov 13 19:55:45 2010 +0100
@@ -147,7 +147,7 @@
         val inp = TextIO.inputAll is
         val _ = TextIO.closeIn is
         val orig_source = Source.of_string inp
-        val symb_source = Symbol.source {do_recover = false} orig_source
+        val symb_source = Symbol.source orig_source
         val lexes =
           (Scan.make_lexicon
             (map Symbol.explode ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"]),

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Nov 13 19:47:23 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Nov 13 19:55:45 2010 +0100
@@ -389,7 +389,7 @@
     val get = maps (ProofContext.get_fact ctxt o fst)
   in
     Source.of_string name
-    |> Symbol.source {do_recover=false}
+    |> Symbol.source
     |> Token.source {do_recover=SOME false} lex Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE