author | wenzelm |
Thu, 30 May 2013 20:20:23 +0200 | |
changeset 52249 | f4bf6b126cab |
parent 52248 | 2c893e0c1def |
child 52250 | 4dced3d4155c |
--- a/src/HOL/Spec_Check/property.ML Thu May 30 20:09:49 2013 +0200 +++ b/src/HOL/Spec_Check/property.ML Thu May 30 20:20:23 2013 +0200 @@ -42,7 +42,7 @@ fun failure (SOME false) = true | failure _ = false -fun apply f x = SOME (f x) handle _ => SOME false (* TODO: do not catch all exceptions! *) +fun apply f x = (case try f x of NONE => SOME false | some => some) fun pred f (x,s) = (apply f x, s) fun pred2 f z = pred (fn x => f (x, z))