changeset 44393 | 23adec5984f1 |
parent 44088 | 3693baa6befb |
child 44394 | 20bd9f90accc |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 22 15:02:45 2011 +0200 @@ -498,7 +498,7 @@ are omitted. *) fun is_dangerous_prop ctxt = transform_elim_prop - #> (has_bound_or_var_of_type (is_type_surely_finite ctxt false) orf + #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) fun int_opt_add (SOME m) (SOME n) = SOME (m + n)