author | haftmann |
Tue, 07 Oct 2008 16:07:30 +0200 | |
changeset 28521 | 5b426c051e36 |
parent 28520 | 376b9c083b04 |
child 28522 | eacb54d9e78d |
--- 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 ())