src/Pure/pattern.ML
changeset 19502 369cde91963d
parent 19482 9f11af8f7ef9
child 19776 a8c02d8b8b40
     1.1 --- a/src/Pure/pattern.ML	Fri Apr 28 17:59:06 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Sat Apr 29 23:16:43 2006 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  
     1.5  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
     1.6  fun mk_proj_list is =
     1.7 -    let fun mk(i::is,j) = if isSome i then j :: mk(is,j-1) else mk(is,j-1)
     1.8 +    let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
     1.9            | mk([],_)    = []
    1.10      in mk(is,length is - 1) end;
    1.11