# HG changeset patch
# User blanchet
# Date 1314436931 -7200
# Node ID 493781b85dcc73e78c25648708d631285e99c101
# Parent  ddfd934e19bbab5f892e054fe303aaca5cec0301# Parent  968115499161c9bd02b96c39cd39c465afc56a02
merged

diff -r ddfd934e19bb -r 493781b85dcc src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 15:11:33 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sat Aug 27 11:22:11 2011 +0200
@@ -117,9 +117,9 @@
 type name = string * string
 
 val type_tag_idempotence =
-  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
+  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
 val type_tag_arguments =
-  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
+  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)
 
 val no_lambdasN = "no_lambdas"
 val concealedN = "concealed"