# HG changeset patch
# User haftmann
# Date 1207309223 -7200
# Node ID 90b02960c8ce78d6d0a4caedf8c8f76a0f9e9caa
# Parent  046e63c9165ccce828eb9327b5d73b1399861c71
prefix for equations in primrec specifications

diff -r 046e63c9165c -r 90b02960c8ce src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Apr 04 13:40:21 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Fri Apr 04 13:40:23 2008 +0200
@@ -244,13 +244,14 @@
         "\nare not mutually recursive");
     val qualify = NameSpace.qualified
       (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];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
-    |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
+    |-> (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 "simps", simp_atts), maps snd simps'))