prefix for equations in primrec specifications
authorhaftmann
Fri Apr 04 13:40:23 2008 +0200 (2008-04-04)
changeset 2655690b02960c8ce
parent 26555 046e63c9165c
child 26557 9e7f95903b24
prefix for equations in primrec specifications
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Apr 04 13:40:21 2008 +0200
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Apr 04 13:40:23 2008 +0200
     1.3 @@ -244,13 +244,14 @@
     1.4          "\nare not mutually recursive");
     1.5      val qualify = NameSpace.qualified
     1.6        (space_implode "_" (map (Sign.base_name o #1) defs));
     1.7 +    val spec' = (map o apfst o apfst) qualify spec;
     1.8      val simp_atts = map (Attrib.internal o K)
     1.9        [Simplifier.simp_add, RecfunCodegen.add NONE];
    1.10    in
    1.11      lthy
    1.12      |> set_group ? LocalTheory.set_group (serial_string ())
    1.13      |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
    1.14 -    |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
    1.15 +    |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
    1.16      |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
    1.17      |-> (fn simps' => LocalTheory.note Thm.theoremK
    1.18            ((qualify "simps", simp_atts), maps snd simps'))