# HG changeset patch
# User haftmann
# Date 1233839643 -3600
# Node ID 4159caa18f85864185fdcd66fcc9c56539505cb3
# Parent  bebe5a254ba6e727be46f31a7f57e31db0d51530
code attribute applied before user attributes

diff -r bebe5a254ba6 -r 4159caa18f85 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Feb 05 14:14:02 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Thu Feb 05 14:14:03 2009 +0100
@@ -247,11 +247,11 @@
     val _ = if gen_eq_set (op =) (names1, names2) then ()
       else primrec_error ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
-    val qualify = Binding.qualify
-      (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, Code.add_default_eqn_attribute];
+    val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
+    val qualify = Binding.qualify prefix;
+    val spec' = (map o apfst)
+      (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
+    val simp_att = (Attrib.internal o K) Simplifier.simp_add;
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
@@ -259,7 +259,7 @@
     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
     |-> (fn simps' => LocalTheory.note Thm.theoremK
-          ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
+          ((qualify (Binding.name "simps"), [simp_att]), maps snd simps'))
     |>> snd
   end handle PrimrecError (msg, some_eqn) =>
     error ("Primrec definition error:\n" ^ msg ^ (case some_eqn