src/HOL/Tools/recfun_codegen.ML
changeset 25570 fdfbbb92dadf
parent 25389 3e58c7cb5a73
child 25894 0ee6e01c5572
equal deleted inserted replaced
25569:c597835d5de4 25570:fdfbbb92dadf
    33 
    33 
    34 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    34 fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
    35   string_of_thm thm);
    35   string_of_thm thm);
    36 
    36 
    37 fun add_thm opt_module thm =
    37 fun add_thm opt_module thm =
    38   if Pattern.pattern (lhs_of thm) then
    38   (if Pattern.pattern (lhs_of thm) then
    39     RecCodegenData.map
    39     RecCodegenData.map
    40       (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
    40       (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
    41   else tap (fn _ => warn thm)
    41   else tap (fn _ => warn thm))
    42   handle TERM _ => tap (fn _ => warn thm);
    42   handle TERM _ => tap (fn _ => warn thm);
    43 
    43 
    44 fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
    44 fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
    45   (add_thm opt_module thm #> Code.add_liberal_func thm) I);
    45   (add_thm opt_module thm #> Code.add_liberal_func thm) I);
    46 
    46