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/recdef_package.ML
changeset 16646 666774b0d1b0
parent 16458 4c6fd0c01d28
child 17057 0934ac31985f 
--- a/src/HOL/Tools/recdef_package.ML	Fri Jul 01 14:13:40 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Jul 01 14:14:40 2005 +0200
@@ -248,7 +248,7 @@
                congs wfs name R eqs;
     val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
     val simp_att = if null tcs then
-      [Simplifier.simp_add_global, RecfunCodegen.add] else [];
+      [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
 
     val (thy, (simps' :: rules', [induct'])) =
       thy
isabelle