# HG changeset patch
# User blanchet
# Date 1314388331 -7200
# Node ID 968115499161c9bd02b96c39cd39c465afc56a02
# Parent  5e681762d53896849d2d2b0cc438147a9c8464b9
change default for generation of tag idempotence and tag argument equations

diff -r 5e681762d538 -r 968115499161 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 08 16:10:49 2010 -0700
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Aug 26 21:52: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"