src/HOL/Tools/polyhash.ML
changeset 28397 389c5e494605
parent 20662 9116dc6842e1
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Tools/polyhash.ML	Mon Sep 29 10:58:04 2008 +0200
     1.2 +++ b/src/HOL/Tools/polyhash.ML	Mon Sep 29 11:46:47 2008 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  			end
     1.5  		  fun bucket n = (copy (Array.sub(arr, n)); bucket (n+1))
     1.6  		  in
     1.7 -		    (bucket 0) handle _ => ();
     1.8 +		    (bucket 0) handle _ => ();  (* FIXME avoid handle _ *)
     1.9  		    table := newArr
    1.10  		  end
    1.11  		else ()
    1.12 @@ -362,7 +362,7 @@
    1.13  		Array.update (newArr, i, Array.sub(arr, i));
    1.14  		mapTbl (i+1))
    1.15  	  in
    1.16 -	    (mapTbl 0) handle _ => ();
    1.17 +	    (mapTbl 0) handle _ => ();  (* FIXME avoid handle _ *)
    1.18  	    HT{hashVal=hashVal, 
    1.19  	       sameKey=sameKey,
    1.20  	       table = ref newArr,