# HG changeset patch
# User berghofe
# Date 1007994855 -3600
# Node ID 473cb9f9e237f2553d616147e77a10d8d31cd82e
# Parent  e752c9aecdece94ea46dc2c9f06801a7f4c6428a
Recursive equations to be used for code generation are now registered
via RecfunCodegen.add

diff -r e752c9aecdec -r 473cb9f9e237 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Dec 10 15:32:10 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Dec 10 15:34:15 2001 +0100
@@ -290,6 +290,7 @@
   (#1 o PureThy.add_thmss [(("simps", simps), []),
     (("", flat case_thms @ size_thms @ 
           flat distinct  @ rec_thms), [Simplifier.simp_add_global]),
+    (("", size_thms @ rec_thms), [RecfunCodegen.add]),
     (("", flat inject),               [iff_add_global]),
     (("", flat distinct RL [notE]),   [Classical.safe_elim_global]),
     (("", weak_case_congs),           [cong_att])]);
diff -r e752c9aecdec -r 473cb9f9e237 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Mon Dec 10 15:32:10 2001 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Mon Dec 10 15:34:15 2001 +0100
@@ -9,13 +9,10 @@
 signature PRIMREC_PACKAGE =
 sig
   val quiet_mode: bool ref
-  val print_primrecs: theory -> unit
-  val get_primrec: theory -> string -> (string * thm list) list option
   val add_primrec: string -> ((bstring * string) * Args.src list) list
     -> theory -> theory * thm list
   val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
     -> theory -> theory * thm list
-  val setup: (theory -> theory) list
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -36,41 +33,6 @@
 fun message s = if ! quiet_mode then () else writeln s;
 
 
-(** theory data **)
-
-(* data kind 'HOL/primrec' *)
-
-structure PrimrecArgs =
-struct
-  val name = "HOL/primrec";
-  type T = (string * thm list) list Symtab.table;
-
-  val empty = Symtab.empty;
-  val copy = I;
-  val prep_ext = I;
-  val merge: T * T -> T = Symtab.merge (K true);
-
-  fun print sg tab =
-    Pretty.writeln (Pretty.strs ("primrecs:" ::
-      map #1 (Sign.cond_extern_table sg Sign.constK tab)));
-end;
-
-structure PrimrecData = TheoryDataFun(PrimrecArgs);
-val print_primrecs = PrimrecData.print;
-
-
-(* get and put data *)
-
-fun get_primrec thy name = Symtab.lookup (PrimrecData.get thy, name);
-
-fun put_primrec name info thy =
-  let val tab = PrimrecData.get thy
-  in 
-    PrimrecData.put (case Symtab.lookup (tab, name) of
-       None => Symtab.update_new ((name, [info]), tab)
-     | Some infos => Symtab.update ((name, info::infos), tab)) thy end;
-
-
 (* preprocessing of equations *)
 
 fun process_eqn sign (eq, rec_fns) = 
@@ -305,12 +267,11 @@
         (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])])
+      |> (#1 o PureThy.add_thmss [(("simps", simps'), [Simplifier.simp_add_global, RecfunCodegen.add])])
       |> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
       |> Theory.parent_path
   in
-    (foldl (fn (thy, (fname, _, _, tname)) =>
-       put_primrec fname (tname, simps) thy) (thy''', defs), simps')
+    (thy''', simps')
   end;
 
 
@@ -328,10 +289,6 @@
   end;
 
 
-(** package setup **)
-
-val setup = [PrimrecData.init];
-
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
diff -r e752c9aecdec -r 473cb9f9e237 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Mon Dec 10 15:32:10 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Mon Dec 10 15:34:15 2001 +0100
@@ -242,7 +242,8 @@
     val (cs, ss, congs, wfs) = prep_hints thy hints;
     val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn strict thy cs ss 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] else [];
+    val simp_att = if null tcs then
+      [Simplifier.simp_add_global, RecfunCodegen.add] else [];
 
     val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
     val (thy, (simps' :: rules', [induct'])) =