Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
authorblanchet
Wed, 20 Jul 2011 00:37:42 +0200
changeset 43906 14d34bd434b8
parent 43905 1ace987e22e5
child 43907 073ab5379842
generate slightly less type information -- this should be sound since type arguments should keep things cleanly apart
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
@@ -1733,7 +1733,7 @@
       1 upto num_args |> map (`I o make_bound_var o string_of_int)
     val bounds =
       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
-    val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
+    val sym_needs_arg_types = exists (curry (op =) dummyT) T_args)
     fun should_keep_arg_type T =
       sym_needs_arg_types orelse
       not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
isabelle