--- 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))
--- 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)) =