src/Pure/pattern.ML

   val eta_contract_atom: term -> term
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   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
   val pattern: term -> bool
   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term

   val envir' = apfst (typ_match thy (pT, oT)) envir;
 in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
 
 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) =
   let fun msub(bounds,obj) = matches thy (pat,obj) orelse
             (case obj of