member (op =);
authorwenzelm
Thu Sep 21 19:05:22 2006 +0200 (2006-09-21)
changeset 20672b96394d8c702
parent 20671 2aa8269a868e
child 20673 27738ccd0700
member (op =);
tuned pattern check;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Thu Sep 21 19:05:08 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Sep 21 19:05:22 2006 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4  fun ints_of []             = []
     1.5    | ints_of (Bound i ::bs) =
     1.6        let val is = ints_of bs
     1.7 -      in if i mem_int is then raise Pattern else i::is end
     1.8 +      in if member (op =) is i then raise Pattern else i::is end
     1.9    | ints_of _              = raise Pattern;
    1.10  
    1.11  fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts);
    1.12 @@ -425,13 +425,13 @@
    1.13                           not(is_Var t)
    1.14    | first_order _ = true;
    1.15  
    1.16 -fun pattern(Abs(_,_,t)) = pattern t
    1.17 -  | pattern(t) = let val (head,args) = strip_comb t
    1.18 -                 in if is_Var head
    1.19 -                    then let val _ = ints_of args in true end
    1.20 -                         handle Pattern => false
    1.21 -                    else forall pattern args
    1.22 -                 end;
    1.23 +fun pattern (Abs (_, _, t)) = pattern t
    1.24 +  | pattern t =
    1.25 +      let val (head, args) = strip_comb t in
    1.26 +        if is_Var head then
    1.27 +          forall is_Bound args andalso not (has_duplicates (op aconv) args)
    1.28 +        else forall pattern args
    1.29 +      end;
    1.30  
    1.31  
    1.32  (* rewriting -- simple but fast *)