removed matches_seq -- didn't quite work;

--- a/src/Pure/pattern.ML	Mon Jun 12 21:19:02 2006 +0200
+++ b/src/Pure/pattern.ML	Mon Jun 12 21:19:03 2006 +0200
@@ -23,7 +23,6 @@
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val matches: theory -> term * term -> bool
-  val matches_seq: theory -> term list -> term list -> bool
   val matches_subterm: theory -> term * term -> bool
   val unify: theory -> term * term -> Envir.env -> Envir.env
   val first_order: term -> bool
@@ -406,14 +405,6 @@
 
 fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
 
-fun matches_seq thy ps os =
-  let
-    fun mtch (pat :: pats) (obj :: objs) env =
-          mtch pats objs (match thy (pairself Envir.beta_norm (Envir.subst_vars env pat, obj)) env)
-      | mtch [] [] env = env
-      | mtch _ _ _ = raise MATCH;
-  in (mtch ps os (Vartab.empty, Vartab.empty); true) handle MATCH => false end;
-
 
 (* Does pat match a subterm of obj? *)
 fun matches_subterm thy (pat,obj) =