--- 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