src/HOL/Tools/record_package.ML

   val record_quick_and_dirty_sensitive: bool ref
   val updateN: string
   val ext_typeN: string
   val last_extT: typ -> (string * typ list) option
   val dest_recTs : typ -> (string * typ list) list
-  val get_extT_fields:  Sign.sg -> typ -> ((string * typ) list * (string * typ))
-  val get_recT_fields:  Sign.sg -> typ -> ((string * typ) list * (string * typ))
-  val get_extension: Sign.sg -> Symtab.key -> (string * typ list) option
-  val get_extinjects: Sign.sg -> thm list
-  val get_simpset: Sign.sg -> simpset
+  val get_extT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
+  val get_recT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
+  val get_extension: theory -> Symtab.key -> (string * typ list) option
+  val get_extinjects: theory -> thm list
+  val get_simpset: theory -> simpset
   val print_records: theory -> unit
-  val add_record: string list * string -> string option -> (string * string * mixfix) list 
-                  -> theory -> theory
-  val add_record_i: string list * string -> (typ list * string) option 
-                    -> (string * typ * mixfix) list -> theory -> theory
+  val add_record: string list * string -> string option -> (string * string * mixfix) list
+    -> theory -> theory
+  val add_record_i: string list * string -> (typ list * string) option
+    -> (string * typ * mixfix) list -> theory -> theory
   val setup: (theory -> theory) list
 end;
 
 
 structure RecordPackage:RECORD_PACKAGE =     

       records sel_upd equalities extinjects extsplit splits extfields fieldext =
  {records = records, sel_upd = sel_upd, 
   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits, 
   extfields = extfields, fieldext = fieldext }: record_data;
 
-structure RecordsArgs =
-struct
+structure RecordsData = TheoryDataFun
+(struct
   val name = "HOL/records";       
   type T = record_data;
 
   val empty =
     make_record_data Symtab.empty
       {selectors = Symtab.empty, updates = Symtab.empty, simpset = HOL_basic_ss}
        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
 
   val copy = I;
-  val prep_ext = I;
-  fun merge
+  val extend = I;
+  fun merge _
    ({records = recs1,
      sel_upd = {selectors = sels1, updates = upds1, simpset = ss1},
      equalities = equalities1,
      extinjects = extinjects1, 
      extsplit = extsplit1,

       fun pretty_record (name, {args, parent, fields, ...}: record_info) =
         Pretty.block (Pretty.fbreaks (Pretty.block
           [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
           pretty_parent parent @ map pretty_field fields));
     in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
-end;
-
-structure RecordsData = TheoryDataFun(RecordsArgs);
+end);
+
 val print_records = RecordsData.print;
+
 
 (* access 'records' *)
 
 fun get_record thy name = Symtab.lookup (#records (RecordsData.get thy), name);
 

       sel_upd equalities extinjects extsplit splits extfields fieldext;
   in RecordsData.put data thy end;
 
 (* access 'sel_upd' *)
 
-fun get_sel_upd sg = #sel_upd (RecordsData.get_sg sg);
+val get_sel_upd = #sel_upd o RecordsData.get;
 
 fun get_selectors sg name = Symtab.lookup (#selectors (get_sel_upd sg), name);
 fun is_selector sg name = 
   case get_selectors sg (Sign.intern_const sg name) of 
      NONE => false

            (Symtab.update_new ((name, thm), equalities)) extinjects extsplit 
            splits extfields fieldext;
   in RecordsData.put data thy end;
 
 fun get_equalities sg name =
-  Symtab.lookup (#equalities (RecordsData.get_sg sg), name);
+  Symtab.lookup (#equalities (RecordsData.get sg), name);
 
 (* access 'extinjects' *)
 
 fun add_extinjects thm thy =
   let

           RecordsData.get thy;
     val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit  
                  splits extfields fieldext;
   in RecordsData.put data thy end;
 
-fun get_extinjects sg = #extinjects (RecordsData.get_sg sg);
+fun get_extinjects sg = #extinjects (RecordsData.get sg);
 
 (* access 'extsplit' *)
 
 fun add_extsplit name thm thy =
   let

       equalities extinjects (Symtab.update_new ((name, thm), extsplit)) splits 
       extfields fieldext;
   in RecordsData.put data thy end;
 
 fun get_extsplit sg name =
-  Symtab.lookup (#extsplit (RecordsData.get_sg sg), name);
+  Symtab.lookup (#extsplit (RecordsData.get sg), name);
 
 (* access 'splits' *)
 
 fun add_record_splits name thmP thy =
   let

       equalities extinjects extsplit (Symtab.update_new ((name, thmP), splits)) 
       extfields fieldext;
   in RecordsData.put data thy end;
 
 fun get_splits sg name =
-  Symtab.lookup (#splits (RecordsData.get_sg sg), name);
+  Symtab.lookup (#splits (RecordsData.get sg), name);
 
 
 
 (* extension of a record name *)
 fun get_extension sg name =
- case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
+ case Symtab.lookup (#records (RecordsData.get sg),name) of
         SOME s => SOME (#extension s)
       | NONE => NONE;
 
 (* access 'extfields' *)
 

          equalities extinjects extsplit splits 
          (Symtab.update_new ((name, fields), extfields)) fieldext;
   in RecordsData.put data thy end;
 
 fun get_extfields sg name =
-  Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
+  Symtab.lookup (#extfields (RecordsData.get sg), name);
 
 fun get_extT_fields sg T = 
   let
     val ((name,Ts),moreT) = dest_recT T;
     val recname = let val (nm::recn::rst) = rev (NameSpace.unpack name) 
                   in NameSpace.pack (rev (nm::rst)) end;
     val midx = maxidx_of_typs (moreT::Ts);
     fun varify (a, S) = TVar ((a, midx), S);
     val varifyT = map_type_tfree varify;
-    val {records,extfields,...} = RecordsData.get_sg sg;
+    val {records,extfields,...} = RecordsData.get sg;
     val (flds,(more,_)) = split_last (Symtab.lookup_multi (extfields,name));
     val args = map varifyT (snd (#extension (valOf (Symtab.lookup (records,recname)))));
 
     val tsig = Sign.tsig_of sg;
     fun unify (t,env) = Type.unify tsig env t;

               splits extfields fieldext';
   in RecordsData.put data thy end;
 
 
 fun get_fieldext sg name =
-  Symtab.lookup (#fieldext (RecordsData.get_sg sg), name);
+  Symtab.lookup (#fieldext (RecordsData.get sg), name);
 
 (* parent records *)
 
 fun add_parents thy NONE parents = parents
   | add_parents thy (SOME (types, name)) parents =

       else opt ();
 
 
 fun prove_split_simp sg T prop =
   let 
-    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get_sg sg;
+    val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
     val extsplits = 
             Library.foldl (fn (thms,(n,_)) => (list (Symtab.lookup (extsplit,n)))@thms) 
                     ([],dest_recTs T);
     val thms = (case get_splits sg (rec_id (~1) T) of
                    SOME (all_thm,_,_,_) => 

       (case t of (sel as Const (s, Type (_,[domS,rangeS])))$((upd as Const (u, _)) $ k $ r)=>
         (case get_selectors sg s of SOME () =>
           (case get_updates sg u of SOME u_name =>
             let
               fun mk_abs_var x t = (x, fastype_of t);
-              val {sel_upd={updates,...},extfields,...} = RecordsData.get_sg sg;
+              val {sel_upd={updates,...},extfields,...} = RecordsData.get sg;
               
               fun mk_eq_terms ((upd as Const (u,Type(_,[updT,_]))) $ k $ r) =
 		  (case (Symtab.lookup (updates,u)) of
                      NONE => NONE
                    | SOME u_name 

 val record_upd_simproc =
   Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
     (fn sg => fn _ => fn t =>
       (case t of ((upd as Const (u, Type(_,[_,Type(_,[T,_])]))) $ k $ r) =>
  	 let datatype ('a,'b) calc = Init of 'b | Inter of 'a  
-             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get_sg sg;
+             val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
              
 	     fun mk_abs_var x t = (x, fastype_of t);
              fun sel_name u = NameSpace.base (unsuffix updateN u);
 
              fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =

  *)
 fun record_split_simp_tac thms P i st =
   let
     val sg = Thm.sign_of_thm st;
     val {sel_upd={simpset,...},...} 
-            = RecordsData.get_sg sg;
+            = RecordsData.get sg;
 
     val has_rec = exists_Const
       (fn (s, Type (_, [Type (_, [T, _]), _])) =>
           (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T 
         | _ => false);