# HG changeset patch
# User paulson
# Date 1156524384 -7200
# Node ID f9cb300118ca801f4cdf3757b5426003669e24cb
# Parent  e3d2d7b01279671c1b01f7e9ff784743e1c227f3
using inc

diff -r e3d2d7b01279 -r f9cb300118ca src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Fri Aug 25 18:45:57 2006 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Fri Aug 25 18:46:24 2006 +0200
@@ -97,7 +97,7 @@
        (*Uses a special character to separate items sent to watcher*)
        TextIO.output (toWatcherStr,
           space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
-       goals_being_watched := (!goals_being_watched) + 1;
+       inc goals_being_watched;
        TextIO.flushOut toWatcherStr;
        callResProvers (toWatcherStr,args))
                                                 
diff -r e3d2d7b01279 -r f9cb300118ca src/HOL/Tools/polyhash.ML
--- a/src/HOL/Tools/polyhash.ML	Fri Aug 25 18:45:57 2006 +0200
+++ b/src/HOL/Tools/polyhash.ML	Fri Aug 25 18:46:24 2006 +0200
@@ -173,7 +173,7 @@
 	  val indx = index (hash, sz)
 	  fun look NIL = (
 		Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
-		n_items := !n_items + 1;
+		inc n_items;
 		growTable tbl;
 		NIL)
 	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
@@ -199,7 +199,7 @@
 	    fun look NIL = 
 		(Array.update(arr, indx, B(hash, key, item, 
 					   Array.sub(arr, indx)));
-		 n_items := !n_items + 1;
+		 inc n_items;
 		 growTable tbl;
 		 NONE)
 	      | look (B(h, k, v, r)) =