diff -r 5fed81762406 -r cee77d2e9582 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Tue Nov 19 19:33:27 2013 +0100 +++ b/src/Pure/Thy/thy_load.ML Tue Nov 19 19:43:26 2013 +0100 @@ -76,7 +76,7 @@ Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => (case Token.get_files tok of [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok) - | files => files)); + | files => map Exn.release files)); (* theory files *) @@ -170,7 +170,9 @@ val lexs = Keyword.get_lexicons (); val toks = Thy_Syntax.parse_tokens lexs text_pos text; - val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks); + val spans = + map (Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir)) + (Thy_Syntax.parse_spans toks); val elements = Thy_Syntax.parse_elements spans; fun init () =