src/Pure/type_infer.ML

 fun polymorphicT T = Type ("_polymorphic_", [T]);
 
 fun pretyp_of is_param (params, typ) =
   let
     fun add_parms (TVar (xi as (x, _), S)) ps =
-          if is_param xi andalso is_none (AList.lookup (op =) ps xi)
+          if is_param xi andalso not (AList.defined (op =) ps xi)
           then (xi, mk_param S) :: ps else ps
       | add_parms (TFree _) ps = ps
       | add_parms (Type (_, Ts)) ps = fold add_parms Ts ps;
 
     val params' = add_parms typ params;

 (* preterm(s)_of *)
 
 fun preterm_of const_type is_param ((vparams, params), tm) =
   let
     fun add_vparm (ps, xi) =
-      if is_none (AList.lookup (op =) ps xi) then
+      if not (AList.defined (op =) ps xi) then
         (xi, mk_param []) :: ps
       else ps;
 
     fun add_vparms (ps, Var (xi, Type ("_polymorphic_", _))) = ps
       | add_vparms (ps, Var (xi, _)) = add_vparm (ps, xi)