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