Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/recfun_codegen.ML
changeset 25389 3e58c7cb5a73
parent 24907 bfb2e82b61fe
child 25570 fdfbbb92dadf 
--- a/src/HOL/Tools/recfun_codegen.ML	Sun Nov 11 14:00:05 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Sun Nov 11 14:00:08 2007 +0100
@@ -37,7 +37,7 @@
 fun add_thm opt_module thm =
   if Pattern.pattern (lhs_of thm) then
     RecCodegenData.map
-      (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
+      (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
   else tap (fn _ => warn thm)
   handle TERM _ => tap (fn _ => warn thm);
isabelle