src/HOL/Tools/function_package/fundef_package.ML
changeset 24624 b8383b1bbae3
parent 24508 c8b82fec6447
child 24626 85eceef2edc7
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:36:14 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:36:15 2007 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4        val tinduct = map remove_domain_condition pinducts
     1.5  
     1.6        val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps
     1.7 -      val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))]
     1.8 +      val allatts = if has_guards then [] else [Attrib.internal (K RecfunCodegen.add_default)]
     1.9  
    1.10        val qualify = NameSpace.qualified defname;
    1.11      in