# HG changeset patch
# User wenzelm
# Date 1150139943 -7200
# Node ID 3a4ca87efdc550963c920925967a3016aea77361
# Parent  7f29aa958b72fe6adaee173e7f2d756c492f3ab5
removed matches_seq -- didn't quite work;

diff -r 7f29aa958b72 -r 3a4ca87efdc5 src/Pure/pattern.ML
--- 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) =