TFL/usyntax.ML
changeset 15531 08c8dad8e399
parent 13182 21851696dbf0
child 16853 33b886cbdc8f
     1.1 --- a/TFL/usyntax.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/TFL/usyntax.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -385,11 +385,11 @@
     1.4  (* Search a term for a sub-term satisfying the predicate p. *)
     1.5  fun find_term p =
     1.6     let fun find tm =
     1.7 -      if (p tm) then Some tm
     1.8 +      if (p tm) then SOME tm
     1.9        else case tm of
    1.10            Abs(_,_,body) => find body
    1.11 -        | (t$u)         => (case find t of None => find u | some => some)
    1.12 -        | _             => None
    1.13 +        | (t$u)         => (case find t of NONE => find u | some => some)
    1.14 +        | _             => NONE
    1.15     in find
    1.16     end;
    1.17