# HG changeset patch # User wenzelm # Date 1237851392 -3600 # Node ID 27ee3f4ea99ca4ad443870f9415b02a5fa01edb7 # Parent 0863bb353065a23ecd80a6653c77b5a1e4540a39 error "Static Errors"; diff -r 0863bb353065 -r 27ee3f4ea99c src/Pure/ML/ml_test.ML --- a/src/Pure/ML/ml_test.ML Tue Mar 24 00:30:52 2009 +0100 +++ b/src/Pure/ML/ml_test.ML Tue Mar 24 00:36:32 2009 +0100 @@ -114,7 +114,7 @@ fun result_fun (parse_tree, code) () = (Context.>> (Result.map (append (the_list parse_tree))); - (case code of NONE => warning "Static Errors" | SOME result => apply_result (result ()))); + (case code of NONE => error "Static Errors" | SOME result => apply_result (result ()))); (* compiler invocation *)