# HG changeset patch
# User berghofe
# Date 1120220080 -7200
# Node ID 666774b0d1b0c7da29699b5f6fa77aab81b18e8a
# Parent  a152d6b21c3174a967c7dcfd5229210ce94b9e35
Adapted to new interface of RecfunCodegen.add.

diff -r a152d6b21c31 -r 666774b0d1b0 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Jul 01 14:13:40 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Jul 01 14:14:40 2005 +0200
@@ -286,7 +286,7 @@
   (#1 o PureThy.add_thmss [(("simps", simps), []),
     (("", List.concat case_thms @ size_thms @ 
           List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
-    (("", size_thms @ rec_thms), [RecfunCodegen.add]),
+    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
     (("", List.concat inject),               [iff_add_global]),
     (("", List.concat distinct RL [notE]),   [Classical.safe_elim_global]),
     (("", weak_case_congs),           [cong_att])]);
diff -r a152d6b21c31 -r 666774b0d1b0 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Jul 01 14:13:40 2005 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Fri Jul 01 14:14:40 2005 +0200
@@ -259,7 +259,8 @@
         (fn _ => [rtac refl 1])) eqns;
     val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
     val thy''' = thy''
-      |> (#1 o PureThy.add_thmss [(("simps", simps'), [Simplifier.simp_add_global, RecfunCodegen.add])])
+      |> (#1 o PureThy.add_thmss [(("simps", simps'),
+           [Simplifier.simp_add_global, RecfunCodegen.add NONE])])
       |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
       |> Theory.parent_path
   in
diff -r a152d6b21c31 -r 666774b0d1b0 src/HOL/Tools/recdef_package.ML
--- 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