proper default codegen attribute
authorhaftmann
Tue, 07 Oct 2008 16:07:30 +0200
changeset 28521 5b426c051e36
parent 28520 376b9c083b04
child 28522 eacb54d9e78d
proper default codegen attribute
src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Tue Oct 07 16:07:25 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Tue Oct 07 16:07:30 2008 +0200
@@ -252,7 +252,7 @@
       (space_implode "_" (map (Sign.base_name o #1) defs));
     val spec' = (map o apfst o apfst) qualify spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, RecfunCodegen.add NONE];
+      [Simplifier.simp_add, RecfunCodegen.add_default];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())