1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 14:42:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Mar 30 16:37:23 2009 +0200
     1.3 @@ -129,9 +129,8 @@
     1.4        val tsimps = map remove_domain_condition psimps
     1.5        val tinduct = map remove_domain_condition pinducts
     1.6  
     1.7 -      val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
     1.8 -      val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
     1.9 -        [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
    1.10 +      val allatts = [Code.add_default_eqn_attrib,
    1.11 +                     Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
    1.12  
    1.13        val qualify = Long_Name.qualify defname;
    1.14      in