# HG changeset patch
# User wenzelm
# Date 1369938023 -7200
# Node ID f4bf6b126cab282493bd8380772552b04e664c5f
# Parent  2c893e0c1defc54042ff20610cfd3ca2e7be2701
do not handle arbitrary exceptions;

diff -r 2c893e0c1def -r f4bf6b126cab src/HOL/Spec_Check/property.ML
--- 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))