# HG changeset patch
# User krauss
# Date 1238423843 -7200
# Node ID 6a3c0ae3fe623243003c6a0481a6a739f9ac9d66
# Parent  5b7a5a05c7aa4f94885107493807ef4580f8b773
optimistically add code attribute to .simps without further checks

diff -r 5b7a5a05c7aa -r 6a3c0ae3fe62 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 14:42:36 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 16:37:23 2009 +0200
@@ -129,9 +129,8 @@
       val tsimps = map remove_domain_condition psimps
       val tinduct = map remove_domain_condition pinducts
 
-      val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
-      val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
-        [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
+      val allatts = [Code.add_default_eqn_attrib,
+                     Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
 
       val qualify = Long_Name.qualify defname;
     in