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