# HG changeset patch
# User haftmann
# Date 1197036476 -3600
# Node ID fdfbbb92dadf7642e3dfc573339290e8cdee6846
# Parent  c597835d5de4af84f65832c8869443aa65b06814
proper treatment of code theorems for primrec

diff -r c597835d5de4 -r fdfbbb92dadf src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Dec 07 15:07:54 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Fri Dec 07 15:07:56 2007 +0100
@@ -258,8 +258,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]
-      @ [Code.add_default_func_attr (*FIXME*)] (*RecfunCodegen.add NONE*);
+    val simp_atts = map (Attrib.internal o K)
+      [Simplifier.simp_add, RecfunCodegen.add NONE];
   in
     lthy
     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
diff -r c597835d5de4 -r fdfbbb92dadf src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Fri Dec 07 15:07:54 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Fri Dec 07 15:07:56 2007 +0100
@@ -35,10 +35,10 @@
   string_of_thm thm);
 
 fun add_thm opt_module thm =
-  if Pattern.pattern (lhs_of thm) then
+  (if Pattern.pattern (lhs_of thm) then
     RecCodegenData.map
       (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
-  else tap (fn _ => warn thm)
+  else tap (fn _ => warn thm))
   handle TERM _ => tap (fn _ => warn thm);
 
 fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping