AList.defined;
authorwenzelm
Tue Sep 06 16:59:57 2005 +0200 (2005-09-06)
changeset 1728243c86fedec82
parent 17281 3b9ff0131ed1
child 17283 881f5873bac0
AList.defined;
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/type_infer.ML	Tue Sep 06 16:59:56 2005 +0200
     1.2 +++ b/src/Pure/type_infer.ML	Tue Sep 06 16:59:57 2005 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4  fun pretyp_of is_param (params, typ) =
     1.5    let
     1.6      fun add_parms (TVar (xi as (x, _), S)) ps =
     1.7 -          if is_param xi andalso is_none (AList.lookup (op =) ps xi)
     1.8 +          if is_param xi andalso not (AList.defined (op =) ps xi)
     1.9            then (xi, mk_param S) :: ps else ps
    1.10        | add_parms (TFree _) ps = ps
    1.11        | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
    1.12 @@ -137,7 +137,7 @@
    1.13  fun preterm_of const_type is_param ((vparams, params), tm) =
    1.14    let
    1.15      fun add_vparm (ps, xi) =
    1.16 -      if is_none (AList.lookup (op =) ps xi) then
    1.17 +      if not (AList.defined (op =) ps xi) then
    1.18          (xi, mk_param []) :: ps
    1.19        else ps;
    1.20