--- 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