using inc
authorpaulson
Fri Aug 25 18:46:24 2006 +0200 (2006-08-25)
changeset 20416f9cb300118ca
parent 20415 e3d2d7b01279
child 20417 c611b1412056
using inc
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/polyhash.ML
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Aug 25 18:45:57 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Aug 25 18:46:24 2006 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4         (*Uses a special character to separate items sent to watcher*)
     1.5         TextIO.output (toWatcherStr,
     1.6            space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
     1.7 -       goals_being_watched := (!goals_being_watched) + 1;
     1.8 +       inc goals_being_watched;
     1.9         TextIO.flushOut toWatcherStr;
    1.10         callResProvers (toWatcherStr,args))
    1.11                                                  
     2.1 --- a/src/HOL/Tools/polyhash.ML	Fri Aug 25 18:45:57 2006 +0200
     2.2 +++ b/src/HOL/Tools/polyhash.ML	Fri Aug 25 18:46:24 2006 +0200
     2.3 @@ -173,7 +173,7 @@
     2.4  	  val indx = index (hash, sz)
     2.5  	  fun look NIL = (
     2.6  		Array.update(arr, indx, B(hash, key, item, Array.sub(arr, indx)));
     2.7 -		n_items := !n_items + 1;
     2.8 +		inc n_items;
     2.9  		growTable tbl;
    2.10  		NIL)
    2.11  	    | look (B(h, k, v, r)) = if ((hash = h) andalso sameKey(key, k))
    2.12 @@ -199,7 +199,7 @@
    2.13  	    fun look NIL = 
    2.14  		(Array.update(arr, indx, B(hash, key, item, 
    2.15  					   Array.sub(arr, indx)));
    2.16 -		 n_items := !n_items + 1;
    2.17 +		 inc n_items;
    2.18  		 growTable tbl;
    2.19  		 NONE)
    2.20  	      | look (B(h, k, v, r)) =