# HG changeset patch
# User wenzelm
# Date 1158858322 -7200
# Node ID b96394d8c702b5307638db059587ba7cb2498868
# Parent  2aa8269a868ec436d519edefa69b4a082d671a97
member (op =);
tuned pattern check;

diff -r 2aa8269a868e -r b96394d8c702 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Sep 21 19:05:08 2006 +0200
+++ b/src/Pure/pattern.ML	Thu Sep 21 19:05:22 2006 +0200
@@ -121,7 +121,7 @@
 fun ints_of []             = []
   | ints_of (Bound i ::bs) =
       let val is = ints_of bs
-      in if i mem_int is then raise Pattern else i::is end
+      in if member (op =) is i then raise Pattern else i::is end
   | ints_of _              = raise Pattern;
 
 fun ints_of' env ts = ints_of (map (Envir.head_norm env) ts);
@@ -425,13 +425,13 @@
                          not(is_Var t)
   | first_order _ = true;
 
-fun pattern(Abs(_,_,t)) = pattern t
-  | pattern(t) = let val (head,args) = strip_comb t
-                 in if is_Var head
-                    then let val _ = ints_of args in true end
-                         handle Pattern => false
-                    else forall pattern args
-                 end;
+fun pattern (Abs (_, _, t)) = pattern t
+  | pattern t =
+      let val (head, args) = strip_comb t in
+        if is_Var head then
+          forall is_Bound args andalso not (has_duplicates (op aconv) args)
+        else forall pattern args
+      end;
 
 
 (* rewriting -- simple but fast *)