src/HOL/Tools/record_package.ML

   val updateN: string
   val mk_fieldT: (string * typ) * typ -> typ
   val dest_fieldT: typ -> (string * typ) * typ
   val dest_fieldTs: typ -> (string * typ) list
   val last_fieldT: typ -> (string * typ) option
+  val last_field: Sign.sg -> string -> (string * typ) option
+  val get_parents: Sign.sg -> string -> string list
   val mk_field: (string * term) * term -> term
   val mk_fst: term -> term
   val mk_snd: term -> term
   val mk_recordT: (string * typ) list * typ -> typ
   val dest_recordT: typ -> (string * typ) list * typ

   val record_upd_simproc: simproc
   val record_split_simproc: (term -> bool) -> simproc
   val record_split_simp_tac: (term -> bool) -> int -> tactic
 end;
 
-structure RecordPackage :RECORD_PACKAGE =
+structure RecordPackage: RECORD_PACKAGE =
 struct
 
 
 (*** theory context references ***)
 

     (fn Const ("unit", _) => true | _ => false) "_record_type" "_record_type_scheme";
 
 
 (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
 (* the (nested) field types.                                                        *)
-fun record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT tm =
+fun record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT tm =
   let
       (* tm is term representation of a (nested) field type. We first reconstruct the      *)
       (* type from tm so that we can continue on the type level rather then the term level.*)
  
       fun get_sort xs n = (case assoc (xs,n) of 

             | _ => record_type_tr' tm)
        else record_type_tr' tm
   end
 
      
-fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT name =
+fun gen_record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT name =
   let val name_sfx = suffix field_typeN name
-      val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF recT rec_schemeT 
+      val tr' = record_type_abbr_tr' sg abbr alphas zeta lastF rec_schemeT 
   in (name_sfx, fn [t,u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
       
 val record_tr' =
   gen_record_tr' "_fields" "_field" fieldN
     (fn Const ("Unity", _) => true | _ => false) "_record" "_record_scheme";

   in RecordsData.put data thy end;
 
 fun get_splits sg name =
   Symtab.lookup (#splits (RecordsData.get_sg sg), name);
 
-
+(* last field of a record *)
+fun last_field sg name =
+      case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
+        Some r => Some (hd (rev (#fields r)))
+      | None => None;
+
+(* get parent names *)
+fun get_parents sg name =
+     (case Symtab.lookup (#records (RecordsData.get_sg sg),name) of
+         Some r => (case #parent r of
+                     Some (_,p) => p::get_parents sg p
+                   | None => [])
+      | None => [])
+       
 (* parent records *)
 
 fun add_parents thy None parents = parents
   | add_parents thy (Some (types, name)) parents =
       let

         conditional (not (null bads)) (fn () =>
           err ("Ill-sorted instantiation of " ^ commas bads ^ " in"));
         add_parents thy parent'
           (make_parent_info name fields' field_inducts field_cases field_splits simps::parents)
       end;
+
 
 
 (** record simprocs **)
  
 fun quick_and_dirty_prove sg xs asms prop tac =

   in foldl_map type_def (theory, names) end;
 
 
 (* field_definitions *)
 
-fun field_definitions fields names xs alphas zeta moreT more vars named_vars thy =
+fun field_definitions fields names alphas zeta moreT more vars thy =
   let
     val sign = Theory.sign_of thy;
     val base = Sign.base_name;
 
     val xT = TFree (variant alphas "'x", HOLogic.typeS);

 
     val field_type_tr's = 
 	let val fldnames = if parent_len = 0 then (tl names) else names;
         in print_translation_field_types (distinct (flat (map NameSpace.accesses' fldnames))) 
         end;
-                          
+
     fun record_type_abbr_tr's thy =
-	let val trnames = (distinct (flat (map NameSpace.accesses' [hd all_names])))
+	let val trnames = NameSpace.accesses' (hd all_names)
             val sg = Theory.sign_of thy
 	in map (gen_record_type_abbr_tr' 
-                 sg bname alphas zeta (hd (rev names)) (recT 0) (rec_schemeT 0)) trnames end;   
+                 sg bname alphas zeta (hd (rev names)) (rec_schemeT 0)) trnames end;   
 
     (* prepare declarations *)
 
     val sel_decls = map (mk_selC (rec_schemeT 0)) bfields @
       [mk_moreC (rec_schemeT 0) (moreN, moreT)];

     (* 1st stage: fields_thy *)
 
     val (fields_thy, field_simps, field_injects, field_splits, field_inducts, field_cases) =
       thy
       |> Theory.add_path bname
-      |> field_definitions fields names xs alphas zeta moreT more vars named_vars;
+      |> field_definitions fields names alphas zeta moreT more vars;
 
     val all_field_inducts = flat (map #field_inducts parents) @ field_inducts;
     val all_field_cases = flat (map #field_cases parents) @ field_cases;
     val all_field_splits = flat (map #field_splits parents) @ field_splits