--- a/src/Pure/General/scan.ML Tue Mar 01 19:42:59 2016 +0100
+++ b/src/Pure/General/scan.ML Tue Mar 01 20:51:38 2016 +0100
@@ -109,7 +109,7 @@
fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
fun permissive scan xs = scan xs handle MORE () => raise FAIL NONE | ABORT _ => raise FAIL NONE;
fun strict scan xs = scan xs handle MORE () => raise FAIL NONE;
-fun error scan xs = scan xs handle ABORT msg => Library.error (msg ());
+fun error scan xs = scan xs handle ABORT msg => Exn.error (msg ());
fun catch scan xs = scan xs
handle ABORT msg => raise Fail (msg ())