removed matches_seq -- didn't quite work;
authorwenzelm
Mon Jun 12 21:19:03 2006 +0200 (2006-06-12)
changeset 198633a4ca87efdc5
parent 19862 7f29aa958b72
child 19864 227a01b8db80
removed matches_seq -- didn't quite work;
src/Pure/pattern.ML
     1.1 --- a/src/Pure/pattern.ML	Mon Jun 12 21:19:02 2006 +0200
     1.2 +++ b/src/Pure/pattern.ML	Mon Jun 12 21:19:03 2006 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4    val first_order_match: theory -> term * term
     1.5      -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
     1.6    val matches: theory -> term * term -> bool
     1.7 -  val matches_seq: theory -> term list -> term list -> bool
     1.8    val matches_subterm: theory -> term * term -> bool
     1.9    val unify: theory -> term * term -> Envir.env -> Envir.env
    1.10    val first_order: term -> bool
    1.11 @@ -406,14 +405,6 @@
    1.12  
    1.13  fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
    1.14  
    1.15 -fun matches_seq thy ps os =
    1.16 -  let
    1.17 -    fun mtch (pat :: pats) (obj :: objs) env =
    1.18 -          mtch pats objs (match thy (pairself Envir.beta_norm (Envir.subst_vars env pat, obj)) env)
    1.19 -      | mtch [] [] env = env
    1.20 -      | mtch _ _ _ = raise MATCH;
    1.21 -  in (mtch ps os (Vartab.empty, Vartab.empty); true) handle MATCH => false end;
    1.22 -
    1.23  
    1.24  (* Does pat match a subterm of obj? *)
    1.25  fun matches_subterm thy (pat,obj) =