Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adaption to CodegenTheorems
authorhaftmann
Tue, 09 May 2006 10:10:12 +0200
changeset 19600 2d969d9a233b
parent 19599 a5c7eb37d14f
child 19601 299d4cd2ef51
adaption to CodegenTheorems
src/HOL/Tools/recfun_codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/recfun_codegen.ML	Tue May 09 10:09:37 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue May 09 10:10:12 2006 +0200
@@ -61,7 +61,7 @@
   end handle TERM _ => (warn thm; thy);
 
 val del = Thm.declaration_attribute
-  (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_def thm))
+  (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_fun thm))
 
 fun del_redundant thy eqs [] = eqs
   | del_redundant thy eqs (eq :: eqs') =
isabelle