# 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 *)