--- a/src/HOL/Tools/primrec_package.ML Thu Dec 06 16:38:42 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML Thu Dec 06 16:56:00 2007 +0100
@@ -257,7 +257,8 @@
"\nare not mutually recursive");
val qualify = NameSpace.qualified
(space_implode "_" (map (Sign.base_name o #1) defs));
- val simp_atts = map (Attrib.internal o K) [Simplifier.simp_add, RecfunCodegen.add NONE];
+ val simp_atts = map (Attrib.internal o K) [Simplifier.simp_add]
+ @ [Code.add_default_func_attr (*FIXME*)] (*RecfunCodegen.add NONE*);
in
lthy
|> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs