# HG changeset patch
# User wenzelm
# Date 1137255651 -3600
# Node ID af605e1864803e031b9eb4bb4b65543e035fa21d
# Parent  cbbc71acf9948e2ad02567f0cec5c5f5eddcbd7c
tuned;

diff -r cbbc71acf994 -r af605e186480 NEWS
--- a/NEWS	Sat Jan 14 17:15:24 2006 +0100
+++ b/NEWS	Sat Jan 14 17:20:51 2006 +0100
@@ -334,7 +334,7 @@
 fixes/assumes or in a locale context).
 
 * ML/Isar: simplified treatment of user-level errors, using exception
-ERROR of string uniformly.  Function now error merely raises ERROR,
+ERROR of string uniformly.  Function error now merely raises ERROR,
 without any side effect on output channels.  The Isar toplevel takes
 care of proper display of ERROR exceptions.  ML code may use plain
 handle/can/try; cat_error may be used to concatenate errors like this:
@@ -342,7 +342,8 @@
   ... handle ERROR msg => cat_error msg "..."
 
 Toplevel ML code (run directly or through the Isar toplevel) may be
-embedded into the Isar exception display/debug facilities as follows:
+embedded into the Isar toplevel with exception display/debug like
+this:
 
   Isar.toplevel (fn () => ...)