# HG changeset patch
# User wenzelm
# Date 1126018797 -7200
# Node ID 43c86fedec8258bac763e18e3a67949cb6a835aa
# Parent  3b9ff0131ed1e3e97db258b55662a09cd29b3c39
AList.defined;

diff -r 3b9ff0131ed1 -r 43c86fedec82 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Tue Sep 06 16:59:56 2005 +0200
+++ b/src/Pure/type_infer.ML	Tue Sep 06 16:59:57 2005 +0200
@@ -111,7 +111,7 @@
 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;
@@ -137,7 +137,7 @@
 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;