paramify_dummies: proper treatment of maxidx;
authorwenzelm
Sat Jan 12 16:38:42 2002 +0100 (2002-01-12 ago)
changeset 127265ae4034883d5
parent 12725 7ede865e1fe5
child 12727 330cb92aaea3
paramify_dummies: proper treatment of maxidx;
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Sat Jan 12 16:37:58 2002 +0100
     1.2 +++ b/src/Pure/type.ML	Sat Jan 12 16:38:42 2002 +0100
     1.3 @@ -857,10 +857,11 @@
     1.4  fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
     1.5  fun param i (x, S) = TVar (("?" ^ x, i), S);
     1.6  
     1.7 -fun paramify_dummies (i, TFree ("'_dummy_", S)) = (i + 1, param i ("'dummy", S))
     1.8 -  | paramify_dummies (i, Type (a, Ts)) =
     1.9 -      let val (i', Ts') = foldl_map paramify_dummies (i, Ts)
    1.10 -      in (i', Type (a, Ts')) end
    1.11 +fun paramify_dummies (maxidx, TFree ("'_dummy_", S)) =
    1.12 +      (maxidx + 1, param (maxidx + 1) ("'dummy", S))
    1.13 +  | paramify_dummies (maxidx, Type (a, Ts)) =
    1.14 +      let val (maxidx', Ts') = foldl_map paramify_dummies (maxidx, Ts)
    1.15 +      in (maxidx', Type (a, Ts')) end
    1.16    | paramify_dummies arg = arg;
    1.17  
    1.18