adapted to new datatypes thy info;

--- a/TFL/thry.sml	Mon Nov 03 21:13:24 1997 +0100
+++ b/TFL/thry.sml	Mon Nov 03 21:15:08 1997 +0100
@@ -53,15 +53,17 @@
      end;
 
 (*---------------------------------------------------------------------------
- * Hacks to make interactive mode work. Referring to "datatypes" directly
- * is temporary, I hope!
+ * Hacks to make interactive mode work.
  *---------------------------------------------------------------------------*)
+
+fun get_info thy ty = Symtab.lookup (ThyData.get_datatypes thy, ty);
+
 val match_info = fn thy =>
     fn "*" => Some({case_const = #case_const (#2 prod_record),
                      constructors = #constructors (#2 prod_record)})
      | "nat" => Some({case_const = #case_const (#2 nat_record),
                        constructors = #constructors (#2 nat_record)})
-     | ty => case assoc(!datatypes,ty)
+     | ty => case get_info thy ty
                of None => None
                 | Some{case_const,constructors, ...} =>
                    Some{case_const=case_const, constructors=constructors}
@@ -71,14 +73,15 @@
                      constructors = #constructors (#2 prod_record)})
      | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
                        constructors = #constructors (#2 nat_record)})
-     | ty => case assoc(!datatypes,ty)
+     | ty => case get_info thy ty
                of None => None
                 | Some{nchotomy,constructors, ...} =>
                   Some{nchotomy=nchotomy, constructors=constructors}
 
 val extract_info = fn thy => 
- let val case_congs = map (#case_cong o #2) (!datatypes)
-         val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
+ let val infos = map snd (Symtab.dest (ThyData.get_datatypes thy));
+     val case_congs = map #case_cong infos;
+     val case_rewrites = flat (map #case_rewrites infos);
  in {case_congs = #case_cong (#2 prod_record)::
                   #case_cong (#2 nat_record)::case_congs,
      case_rewrites = #case_rewrites(#2 prod_record)@

--- a/src/HOL/datatype.ML	Mon Nov 03 21:13:24 1997 +0100
+++ b/src/HOL/datatype.ML	Mon Nov 03 21:15:08 1997 +0100
@@ -3,41 +3,36 @@
    Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
                 Konrad Slind
    Copyright 1995 TU Muenchen
-
 *)
 
-(** Information about datatypes **)
+
+(** theory information about datatypes **)
 
-(* Retrieve information for a specific datatype *)
-fun datatype_info thy tname =
-  case get_thydata (Sign.name_of (sign_of thy)) "datatypes" of
-      None => None
-    | Some (DT_DATA ds) => assoc (ds, tname);
+fun datatype_info_sg sg name =
+  (case Symtab.lookup (ThyData.get_datatypes_sg sg, name) of
+    Some info => info
+  | None => error ("Unknown datatype " ^ quote name));
 
-fun match_info thy tname =
-  case datatype_info thy tname of
-      Some {case_const, constructors, ...} =>
-        {case_const=case_const, constructors=constructors}
-    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
+val datatype_info = datatype_info_sg o sign_of;
 
-fun induct_info thy tname =
-  case datatype_info thy tname of
-      Some {constructors, nchotomy, ...} =>
-        {constructors=constructors, nchotomy=nchotomy}
-    | None => error ("No datatype \"" ^ tname ^ "\" defined in this theory.");
-
+fun match_info thy name =
+  let val {case_const, constructors, ...} = datatype_info thy name in
+    {case_const = case_const, constructors = constructors}
+  end;
 
-(* Retrieve information for all datatypes defined in a theory and its
-   ancestors *)
+fun induct_info thy name =
+  let val {constructors, nchotomy, ...} = datatype_info thy name in
+    {constructors = constructors, nchotomy = nchotomy}
+  end;
+
+(*retrieve information for all datatypes defined in a theory*)
 fun extract_info thy =
-  let val (congs, rewrites) =
-        case get_thydata (Sign.name_of (sign_of thy)) "datatypes" of
-            None => ([], [])
-          | Some (DT_DATA ds) =>
-              let val info = map snd ds
-              in (map #case_cong info, flat (map #case_rewrites info)) end;
+  let
+    val infos = map snd (Symtab.dest (ThyData.get_datatypes thy));
+    val (congs, rewrites) = (map #case_cong infos, flat (map #case_rewrites infos));
   in {case_congs = congs, case_rewrites = rewrites} end;
 
+
 local
 
 fun find_tname var Bi =
@@ -49,14 +44,6 @@
      | _ => error("Cannot induct on type of " ^ quote var)
   end;
 
-fun get_dt_info sign tn =
-      case get_thydata (Sign.name_of sign) "datatypes" of
-        None => error ("No such datatype: " ^ quote tn)
-      | Some (DT_DATA ds) =>
-          case assoc (ds, tn) of
-            Some info => info
-          | None => error ("Not a datatype: " ^ quote tn)
-
 fun infer_tname state sign i aterm =
 let val (_, _, Bi, _) = dest_state (state, i)
     val params = Logic.strip_params Bi	        (*params of subgoal i*)
@@ -78,14 +65,14 @@
         let val (_, _, Bi, _) = dest_state (state, i)
             val sign = #sign(rep_thm state)
             val tn = find_tname var Bi
-            val ind_tac = #induct_tac(get_dt_info sign tn)
+            val ind_tac = #induct_tac(datatype_info_sg sign tn)
         in ind_tac var i end;
 
 (* generic exhaustion tactic for datatypes *)
 fun exhaust_tac aterm i state = state |>
         let val sign = #sign(rep_thm state)
             val tn = infer_tname state sign i aterm
-            val exh_tac = #exhaust_tac(get_dt_info sign tn)
+            val exh_tac = #exhaust_tac(datatype_info_sg sign tn)
         in exh_tac aterm i end;
 
 end;
@@ -640,10 +627,10 @@
   val case_thms : Sign.sg -> thm list -> (string -> int -> tactic)
                    -> {nchotomy:thm, case_cong:thm}
 
-  val build_record : (theory * (string * string list)
-                      * (string -> int -> tactic))
-                     -> (string * dtype_info) 
-
+  val build_record: theory * (string * string list) * (string -> int -> tactic)
+    -> string * datatype_info
+  val add_record: string * string list * (string -> int -> tactic) -> theory -> theory
+  val add_datatype_info: string * datatype_info -> theory -> theory
 end;
 
 
@@ -1004,6 +991,15 @@
 end;
 
 
+fun add_datatype_info info thy = thy |>
+  ThyData.put_datatypes (Symtab.update (info, ThyData.get_datatypes thy));
+
+fun add_record (ty, cl, itac) thy = thy |>
+  add_datatype_info (build_record (thy, (ty, cl), itac));
+
+
+
+
 (*---------------------------------------------------------------------------
  * Test
  *