src/HOL/Tools/recfun_codegen.ML
changeset 25570 fdfbbb92dadf
parent 25389 3e58c7cb5a73
child 25894 0ee6e01c5572
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Fri Dec 07 15:07:54 2007 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Fri Dec 07 15:07:56 2007 +0100
     1.3 @@ -35,10 +35,10 @@
     1.4    string_of_thm thm);
     1.5  
     1.6  fun add_thm opt_module thm =
     1.7 -  if Pattern.pattern (lhs_of thm) then
     1.8 +  (if Pattern.pattern (lhs_of thm) then
     1.9      RecCodegenData.map
    1.10        (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
    1.11 -  else tap (fn _ => warn thm)
    1.12 +  else tap (fn _ => warn thm))
    1.13    handle TERM _ => tap (fn _ => warn thm);
    1.14  
    1.15  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping