diff -r b0cd55afead1 -r d4a35f82fbb4 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/pattern.ML	Tue Oct 04 19:01:37 2005 +0200
@@ -444,12 +444,12 @@
 (* 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
+            (case obj of
               Abs(x,T,t) => let val y = 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
+            | _ => false)
   in msub([],obj) end;
 
 fun first_order(Abs(_,_,t)) = first_order t