src/Pure/pattern.ML
changeset 17756 d4a35f82fbb4
parent 17412 e26cb20ef0cc
child 18011 685d95c793ff
     1.1 --- a/src/Pure/pattern.ML	Tue Oct 04 16:47:40 2005 +0200
     1.2 +++ b/src/Pure/pattern.ML	Tue Oct 04 19:01:37 2005 +0200
     1.3 @@ -444,12 +444,12 @@
     1.4  (* Does pat match a subterm of obj? *)
     1.5  fun matches_subterm thy (pat,obj) =
     1.6    let fun msub(bounds,obj) = matches thy (pat,obj) orelse
     1.7 -            case obj of
     1.8 +            (case obj of
     1.9                Abs(x,T,t) => let val y = variant bounds x
    1.10                                  val f = Free(":" ^ y,T)
    1.11                              in msub(x::bounds,subst_bound(f,t)) end
    1.12              | s$t => msub(bounds,s) orelse msub(bounds,t)
    1.13 -            | _ => false
    1.14 +            | _ => false)
    1.15    in msub([],obj) end;
    1.16  
    1.17  fun first_order(Abs(_,_,t)) = first_order t