'HOL/recdef' theory data;

--- a/src/HOL/Tools/recdef_package.ML	Fri Apr 16 14:49:06 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Fri Apr 16 14:49:09 1999 +0200
@@ -8,28 +8,71 @@
 signature RECDEF_PACKAGE =
 sig
   val quiet_mode: bool ref
+  val print_recdefs: theory -> unit
+  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list}
   val add_recdef: xstring -> string -> ((bstring * string) * Args.src list) list
     -> string option -> (xstring * Args.src list) list
     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
   val add_recdef_i: xstring -> term -> ((bstring * term) * theory attribute list) list
     -> simpset option -> (thm * theory attribute list) list
     -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
+  val setup: (theory -> theory) list
 end;
 
 structure RecdefPackage: RECDEF_PACKAGE =
 struct
 
-
-(* messages *)
-
 val quiet_mode = Tfl.quiet_mode;
 val message = Tfl.message;
 
 
-(* add_recdef(_i) *)
+
+(** theory data **)
+
+(* data kind 'HOL/recdef' *)
+
+type recdef_info = {rules: thm list, induct: thm, tcs: term list};
+
+structure RecdefArgs =
+struct
+  val name = "HOL/recdef";
+  type T = recdef_info Symtab.table;
+
+  val empty = Symtab.empty;
+  val prep_ext = I;
+  val merge: T * T -> T = Symtab.merge (K true);
+
+  fun print sg tab =
+    Pretty.writeln (Pretty.strs ("recdefs:" ::
+      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
+end;
+
+structure RecdefData = TheoryDataFun(RecdefArgs);
+val print_recdefs = RecdefData.print;
 
-fun gen_add_recdef tfl_def prep_att prep_ss app_thms name R eq_srcs raw_ss raw_congs thy =
+
+(* get and put data *)
+
+fun get_recdef thy name =
+  (case Symtab.lookup (RecdefData.get thy, name) of
+    Some info => info
+  | None => error ("Unknown recursive function " ^ quote name));
+
+fun put_recdef name info thy =
   let
+    val tab = Symtab.update_new ((name, info), RecdefData.get thy)
+      handle Symtab.DUP _ => error ("Duplicate recursive function definition " ^ quote name);
+  in RecdefData.put tab thy end;
+
+
+
+(** add_recdef(_i) **)
+
+fun gen_add_recdef tfl_def prep_att prep_ss app_thms raw_name R eq_srcs raw_ss raw_congs thy =
+  let
+    val name = Sign.intern_const (Theory.sign_of thy) raw_name;
+    val bname = Sign.base_name name;
+
     val _ = message ("Defining recursive function " ^ quote name ^ " ...");
 
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
@@ -40,9 +83,10 @@
     val (result as {rules, induct, tcs}) = Tfl.simplify_defn (ss, congs) (thy2, (name, pats));
     val thy3 =
       thy2
-      |> Theory.add_path name
+      |> Theory.add_path bname
       |> PureThy.add_thmss [(("rules", rules), [])]
       |> PureThy.add_thms ((("induct", induct), []) :: ((eq_names ~~ rules) ~~ eq_atts))
+      |> put_recdef name result
       |> Theory.parent_path;
   in (thy3, result) end;
 
@@ -52,6 +96,13 @@
 val add_recdef_i = gen_add_recdef Tfl.define_i (K I) I IsarThy.apply_theorems_i;
 
 
+(** package setup **)
+
+(* setup theory *)
+
+val setup = [RecdefData.init];
+
+
 (* outer syntax *)
 
 local open OuterParse in
@@ -63,7 +114,7 @@
   >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef f R (map triple_swap eqs) ss congs);
 
 val recdefP =
-  OuterSyntax.command "recdef" "general recursive function definition (TFL)"
+  OuterSyntax.command "recdef" "define general recursive functions (TFL)"
     (recdef_decl >> Toplevel.theory);
 
 val _ = OuterSyntax.add_keywords ["congs", "simpset"];