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
+  val get_recT_fields:  Sign.sg -> typ -> (string * typ) list
   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 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

   in RecordsData.put data thy end;
 
 fun get_extfields sg name =
   Symtab.lookup (#extfields (RecordsData.get_sg sg), name);
 
+fun get_extT_fields sg T = 
+  let val {extfields,...} = RecordsData.get_sg sg;
+  in Symtab.lookup_multi (extfields,fst (fst (dest_recT T)))
+  end; 
+
+fun get_fields extfields T = 
+     foldl (fn (xs,(eN,_))=>xs@(Symtab.lookup_multi (extfields,eN)))
+             ([],(dest_recTs T));
+
+fun get_recT_fields sg T = 
+  let val {extfields,...} = RecordsData.get_sg sg;
+  in get_fields extfields T
+  end;
+
 (* access 'fieldext' *)
 
 fun add_fieldext extname_types fields thy =
   let
     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} = 

         end
    | _ => error "RecordPackage.prove_split_simp:code should never been reached")
 
 
 
-local
-fun get_fields extfields T = 
-     foldl (fn (xs,(eN,_))=>xs@(map fst (Symtab.lookup_multi (extfields,eN))))
-             ([],(dest_recTs T));
-in
+
 (* record_simproc *)
 (* Simplifies selections of an record update:
  *  (1)  S (r(|S:=k|)) = k respectively
  *  (2)  S (r(|X:=k|)) = S r
  * The simproc skips multiple updates at once, eg:

                                val rv = mk_abs_var "r" r
                                val rb = Bound 0
                                val kv = mk_abs_var "k" k
                                val kb = Bound 1 
                              in Some (upd$kb$rb,kb,[kv,rv],true) end
-                        else if u_name mem (get_fields extfields rangeS)
-                             orelse s mem (get_fields extfields updT)
+                        else if u_name mem (map fst (get_fields extfields rangeS))
+                             orelse s mem (map fst (get_fields extfields updT))
                              then None
 			     else (case mk_eq_terms r of 
                                      Some (trm,trm',vars,update_s) 
                                      => let   
 					  val kv = mk_abs_var "k" k

              
 	     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) =
-                  if s mem (get_fields extfields mT) then upd else seed s r
+                  if s mem (map fst (get_fields extfields mT)) then upd else seed s r
                | seed _ r = r;
 
              fun grow u uT k vars (sprout,skeleton) = 
 		   if sel_name u = moreN
                    then let val kv = mk_abs_var "k" k;

                 => Some (prove_split_simp sg T  
                           (list_all(vars,(Logic.mk_equals (trm,trm')))))
              | _ => None)
 	 end
        | _ => None));
-end
 
 (* record_eq_simproc *)
 (* looks up the most specific record-equality.
  * Note on efficiency:
  * Testing equality of records boils down to the test of equality of all components.

     val all_variants = parent_variants @ variants;
     val all_vars = parent_vars @ vars;
     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
 
 
-    val zeta = variant alphas "'z";
+    val zeta = variant alphas "'z"; 
     val moreT = TFree (zeta, HOLogic.typeS);
     val more = Free (moreN, moreT);
     val full_moreN = full moreN;
     val bfields_more = bfields @ [(moreN,moreT)];
     val fields_more = fields @ [(full_moreN,moreT)];