# HG changeset patch
# User wenzelm
# Date 1203271490 -3600
# Node ID 9b48d0264ffd07b8926c50a5ec098a0be4cc5d4b
# Parent  454a5456a4b52dd96772926a9622cb62bc88992f
added get_parent (for AWE);
tuned;

diff -r 454a5456a4b5 -r 9b48d0264ffd src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sun Feb 17 18:43:17 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Sun Feb 17 19:04:50 2008 +0100
@@ -37,9 +37,10 @@
 
   val last_extT: typ -> (string * typ list) option
   val dest_recTs : typ -> (string * typ list) list
-  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_extT_fields:  theory -> typ -> (string * typ) list * (string * typ)
+  val get_recT_fields:  theory -> typ -> (string * typ) list * (string * typ)
+  val get_parent: theory -> string -> (typ list * string) option
+  val get_extension: theory -> string -> (string * typ list) option
   val get_extinjects: theory -> thm list
   val get_simpset: theory -> simpset
   val print_records: theory -> unit
@@ -406,6 +407,7 @@
 
 val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
 
+
 (* access 'splits' *)
 
 fun add_record_splits name thmP thy =
@@ -420,10 +422,10 @@
 val get_splits = Symtab.lookup o #splits o RecordsData.get;
 
 
+(* parent/extension of named record *)
 
-(* extension of a record name *)
-val get_extension =
-  Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
+val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o RecordsData.get);
+val get_extension = Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
 
 
 (* access 'extfields' *)