diff -r 39d01eaf5292 -r 7187cb7a77c5 src/Pure/General/scan.ML
--- 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 ())