src/HOL/Tools/record_package.ML
changeset 26088 9b48d0264ffd
parent 26065 d80a49f51b94
child 26164 429c1917f07b
     1.1 --- a/src/HOL/Tools/record_package.ML	Sun Feb 17 18:43:17 2008 +0100
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sun Feb 17 19:04:50 2008 +0100
     1.3 @@ -37,9 +37,10 @@
     1.4  
     1.5    val last_extT: typ -> (string * typ list) option
     1.6    val dest_recTs : typ -> (string * typ list) list
     1.7 -  val get_extT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
     1.8 -  val get_recT_fields:  theory -> typ -> ((string * typ) list * (string * typ))
     1.9 -  val get_extension: theory -> Symtab.key -> (string * typ list) option
    1.10 +  val get_extT_fields:  theory -> typ -> (string * typ) list * (string * typ)
    1.11 +  val get_recT_fields:  theory -> typ -> (string * typ) list * (string * typ)
    1.12 +  val get_parent: theory -> string -> (typ list * string) option
    1.13 +  val get_extension: theory -> string -> (string * typ list) option
    1.14    val get_extinjects: theory -> thm list
    1.15    val get_simpset: theory -> simpset
    1.16    val print_records: theory -> unit
    1.17 @@ -406,6 +407,7 @@
    1.18  
    1.19  val get_extsplit = Symtab.lookup o #extsplit o RecordsData.get;
    1.20  
    1.21 +
    1.22  (* access 'splits' *)
    1.23  
    1.24  fun add_record_splits name thmP thy =
    1.25 @@ -420,10 +422,10 @@
    1.26  val get_splits = Symtab.lookup o #splits o RecordsData.get;
    1.27  
    1.28  
    1.29 +(* parent/extension of named record *)
    1.30  
    1.31 -(* extension of a record name *)
    1.32 -val get_extension =
    1.33 -  Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
    1.34 +val get_parent = (Option.join o Option.map #parent) oo (Symtab.lookup o #records o RecordsData.get);
    1.35 +val get_extension = Option.map #extension oo (Symtab.lookup o #records o RecordsData.get);
    1.36  
    1.37  
    1.38  (* access 'extfields' *)