# HG changeset patch
# User wenzelm
# Date 1289674545 -3600
# Node ID ca3c6b1bfcdb9ce490719e0decf06aab51a3d561
# Parent  14a2e686bdac1764a92e28a2b8051ceaa7923aae
total Symbol.source;

diff -r 14a2e686bdac -r ca3c6b1bfcdb src/HOL/Import/import_syntax.ML
--- 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"]),
diff -r 14a2e686bdac -r ca3c6b1bfcdb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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