242 val _ = if gen_eq_set (op =) (names1, names2) then () |
242 val _ = if gen_eq_set (op =) (names1, names2) then () |
243 else primrec_error ("functions " ^ commas_quote names2 ^ |
243 else primrec_error ("functions " ^ commas_quote names2 ^ |
244 "\nare not mutually recursive"); |
244 "\nare not mutually recursive"); |
245 val qualify = NameSpace.qualified |
245 val qualify = NameSpace.qualified |
246 (space_implode "_" (map (Sign.base_name o #1) defs)); |
246 (space_implode "_" (map (Sign.base_name o #1) defs)); |
|
247 val spec' = (map o apfst o apfst) qualify spec; |
247 val simp_atts = map (Attrib.internal o K) |
248 val simp_atts = map (Attrib.internal o K) |
248 [Simplifier.simp_add, RecfunCodegen.add NONE]; |
249 [Simplifier.simp_add, RecfunCodegen.add NONE]; |
249 in |
250 in |
250 lthy |
251 lthy |
251 |> set_group ? LocalTheory.set_group (serial_string ()) |
252 |> set_group ? LocalTheory.set_group (serial_string ()) |
252 |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs |
253 |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs |
253 |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec)) |
254 |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec')) |
254 |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps) |
255 |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps) |
255 |-> (fn simps' => LocalTheory.note Thm.theoremK |
256 |-> (fn simps' => LocalTheory.note Thm.theoremK |
256 ((qualify "simps", simp_atts), maps snd simps')) |
257 ((qualify "simps", simp_atts), maps snd simps')) |
257 |>> snd |
258 |>> snd |
258 end handle PrimrecError (msg, some_eqn) => |
259 end handle PrimrecError (msg, some_eqn) => |