--- 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