src/HOL/Tools/primrec_package.ML
changeset 25570 fdfbbb92dadf
parent 25566 33f740c5e022
child 25604 6c1714b9b805
equal deleted inserted replaced
25569:c597835d5de4 25570:fdfbbb92dadf
   256     val _ = if gen_eq_set (op =) (names1, names2) then ()
   256     val _ = if gen_eq_set (op =) (names1, names2) then ()
   257       else primrec_error ("functions " ^ commas_quote names2 ^
   257       else primrec_error ("functions " ^ commas_quote names2 ^
   258         "\nare not mutually recursive");
   258         "\nare not mutually recursive");
   259     val qualify = NameSpace.qualified
   259     val qualify = NameSpace.qualified
   260       (space_implode "_" (map (Sign.base_name o #1) defs));
   260       (space_implode "_" (map (Sign.base_name o #1) defs));
   261     val simp_atts = map (Attrib.internal o K) [Simplifier.simp_add]
   261     val simp_atts = map (Attrib.internal o K)
   262       @ [Code.add_default_func_attr (*FIXME*)] (*RecfunCodegen.add NONE*);
   262       [Simplifier.simp_add, RecfunCodegen.add NONE];
   263   in
   263   in
   264     lthy
   264     lthy
   265     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
   265     |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
   266     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
   266     |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
   267     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
   267     |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)