# HG changeset patch
# User wenzelm
# Date 1191882416 -7200
# Node ID 2a49fc046dc089d433a714d5eccb8bef93c02806
# Parent  9e095546cdac54eeb407f3077f3cee2af189ce21
tuned;

diff -r 9e095546cdac -r 2a49fc046dc0 NEWS
--- a/NEWS	Tue Oct 09 00:20:23 2007 +0200
+++ b/NEWS	Tue Oct 09 00:26:56 2007 +0200
@@ -1311,8 +1311,8 @@
 (Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
 with common combinations (Syntax.pretty_term, Syntax.string_of_term
 etc.).  Former Sign.pretty_term, Sign.string_of_term etc. are still
-available for convenience, but refer to the very same operations
-(using a mere theory instead of a full context).
+available for convenience, but refer to the very same operations using
+a mere theory instead of a full context.
 
 * Isar: simplified treatment of user-level errors, using exception
 ERROR of string uniformly.  Function error now merely raises ERROR,