src/Pure/pattern.ML
changeset 4667 6328d427a339
parent 2792 6c17c5ec3d8b
child 4820 8f6dbbd8d497
     1.1 --- a/src/Pure/pattern.ML	Fri Feb 27 11:21:28 1998 +0100
     1.2 +++ b/src/Pure/pattern.ML	Sat Feb 28 15:40:03 1998 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4    val match             : type_sig -> term * term
     1.5                            -> (indexname*typ)list * (indexname*term)list
     1.6    val matches           : type_sig -> term * term -> bool
     1.7 +  val matches_subterm   : type_sig -> term * term -> bool
     1.8    val unify             : sg * env * (term * term)list -> env
     1.9    exception Unif
    1.10    exception MATCH
    1.11 @@ -390,4 +391,15 @@
    1.12  (*Predicate: does the pattern match the object?*)
    1.13  fun matches tsig po = (match tsig po; true) handle MATCH => false;
    1.14  
    1.15 +(* Does pat match a subterm of obj? *)
    1.16 +fun matches_subterm tsig (pat,obj) =
    1.17 +  let fun msub(bounds,obj) = matches tsig (pat,obj) orelse
    1.18 +            case obj of
    1.19 +              Abs(x,T,t) => let val y = variant bounds x
    1.20 +                                val f = Free(":" ^ y,T)
    1.21 +                            in msub(x::bounds,subst_bound(f,t)) end
    1.22 +            | s$t => msub(bounds,s) orelse msub(bounds,t)
    1.23 +            | _ => false
    1.24 +  in msub([],obj) end;
    1.25 +
    1.26  end;