diff -r 01fa6e7e7196 -r 2270829d2364 TFL/thry.sml
--- 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)@