diff -r 9afa7183dfc2 -r 369cde91963d src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/pattern.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -153,7 +153,7 @@
 
 (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
 fun mk_proj_list is =
-    let fun mk(i::is,j) = if isSome i then j :: mk(is,j-1) else mk(is,j-1)
+    let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
           | mk([],_)    = []
     in mk(is,length is - 1) end;