Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
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)
isabelle