# HG changeset patch
# User haftmann
# Date 1196956560 -3600
# Node ID f0fc8531c9097fb7f015eccf1c092e394e0b2ae1
# Parent  d955e1d01e6a4a044fcfab12162773dbbb3a506f
fixed slip

diff -r d955e1d01e6a -r f0fc8531c909 src/HOL/Tools/primrec_package.ML
--- 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