diff -r 1ffe739e5ee0 -r c5b93c69afd3 src/Provers/order.ML
--- a/src/Provers/order.ML	Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Provers/order.ML	Thu Jul 05 00:06:14 2007 +0200
@@ -644,7 +644,7 @@
 	  val yi = getIndex y ntc 
 	  
 	  fun lookup k [] =  raise Cannot
-	  |   lookup k ((h,l)::us) = if k = h then l else lookup k us;	  
+	  |   lookup k ((h: int,l)::us) = if k = h then l else lookup k us;	  
 	  
 	  fun rev_completeComponentPath y' = 
 	   let val edge = lookup (getIndex y' ntc) predlist
@@ -974,7 +974,7 @@
                     - it is a <= edge and no parallel < edge was found earlier
                     - it is a < edge
                  *)
-          	 fun insert (h,l) [] = [(h,l)]
+          	 fun insert (h: int,l) [] = [(h,l)]
 		 |   insert (h,l) ((k',l')::es) = if h = k' then (
 		     case l of (Less (_, _, _)) => (h,l)::es
 		     | _  => (case l' of (Less (_, _, _)) => (h,l')::es