# HG changeset patch
# User wenzelm
# Date 1170786752 -3600
# Node ID 8fcd11cb9be73539da0dbabe3dc10ccb6bae98a8
# Parent  420625970f31fa4286b988285360349b05a4f4c9
tuned matches_subterm;

diff -r 420625970f31 -r 8fcd11cb9be7 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Feb 06 19:32:31 2007 +0100
+++ b/src/Pure/pattern.ML	Tue Feb 06 19:32:32 2007 +0100
@@ -410,15 +410,14 @@
 
 
 (* 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
-              Abs(x,T,t) => let val y = Name.variant bounds x
-                                val f = Free(":" ^ y,T)
-                            in msub(x::bounds,subst_bound(f,t)) end
-            | s$t => msub(bounds,s) orelse msub(bounds,t)
-            | _ => false)
-  in msub([],obj) end;
+fun matches_subterm thy (pat, obj) =
+  let
+    fun msub bounds obj = matches thy (pat, obj) orelse
+      (case obj of
+        Abs (x, T, t) => msub (bounds + 1) (snd (Term.dest_abs (Name.bound bounds, T, t)))
+      | t $ u => msub bounds t orelse msub bounds u
+      | _ => false)
+  in msub 0 obj end;
 
 fun first_order(Abs(_,_,t)) = first_order t
   | first_order(t $ u) = first_order t andalso first_order u andalso