src/Pure/consts.ML
changeset 32784 1a5dde5079ac
parent 31977 e03059ae2d82
child 33092 c859019d3ac5
     1.1 --- a/src/Pure/consts.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/consts.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  
     1.5  fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is
     1.6    | subscript T [] = T
     1.7 -  | subscript T _ = raise Subscript;
     1.8 +  | subscript _ _ = raise Subscript;
     1.9  
    1.10  in
    1.11