proper treatment of code theorems for primrec
authorhaftmann
Fri Dec 07 15:07:56 2007 +0100 (2007-12-07)
changeset 25570fdfbbb92dadf
parent 25569 c597835d5de4
child 25571 c9e39eafc7a0
proper treatment of code theorems for primrec
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recfun_codegen.ML
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Dec 07 15:07:54 2007 +0100
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Dec 07 15:07:56 2007 +0100
     1.3 @@ -258,8 +258,8 @@
     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 simp_atts = map (Attrib.internal o K) [Simplifier.simp_add]
     1.8 -      @ [Code.add_default_func_attr (*FIXME*)] (*RecfunCodegen.add NONE*);
     1.9 +    val simp_atts = map (Attrib.internal o K)
    1.10 +      [Simplifier.simp_add, RecfunCodegen.add NONE];
    1.11    in
    1.12      lthy
    1.13      |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
     2.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Dec 07 15:07:54 2007 +0100
     2.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Dec 07 15:07:56 2007 +0100
     2.3 @@ -35,10 +35,10 @@
     2.4    string_of_thm thm);
     2.5  
     2.6  fun add_thm opt_module thm =
     2.7 -  if Pattern.pattern (lhs_of thm) then
     2.8 +  (if Pattern.pattern (lhs_of thm) then
     2.9      RecCodegenData.map
    2.10        (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
    2.11 -  else tap (fn _ => warn thm)
    2.12 +  else tap (fn _ => warn thm))
    2.13    handle TERM _ => tap (fn _ => warn thm);
    2.14  
    2.15  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping