diff -r 83308748c5ae -r 9a64c4007864 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Jan 15 15:37:49 2011 +0100
+++ b/src/HOL/Tools/record.ML	Sat Jan 15 16:49:10 2011 +0100
@@ -25,6 +25,7 @@
     cases: thm, simps: thm list, iffs: thm list}
   val get_info: theory -> string -> info option
   val the_info: theory -> string -> info
+  val get_hierarchy: theory -> (string * typ list) -> (string * (string * typ) list) list
   val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
     (binding * typ * mixfix) list -> theory -> theory
 
@@ -614,12 +615,14 @@
 
 (* parent records *)
 
-fun add_parents _ NONE parents = parents
-  | add_parents thy (SOME (types, name)) parents =
+local
+
+fun add_parents _ NONE = I
+  | add_parents thy (SOME (types, name)) =
       let
         fun err msg = error (msg ^ " parent record " ^ quote name);
 
-        val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
+        val {args, parent, ...} =
           (case get_info thy name of SOME info => info | NONE => err "Unknown");
         val _ = if length types <> length args then err "Bad number of arguments for" else ();
 
@@ -631,12 +634,22 @@
         val inst = map fst args ~~ types;
         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
         val parent' = Option.map (apfst (map subst)) parent;
-        val fields' = map (apsnd subst) fields;
-        val extension' = apsnd (map subst) extension;
-      in
-        add_parents thy parent'
-          (make_parent_info name fields' extension' ext_def induct_scheme :: parents)
-      end;
+      in cons (name, inst) #> add_parents thy parent' end;
+
+in
+
+fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
+
+fun get_parent_info thy parent =
+  add_parents thy parent [] |> map (fn (name, inst) =>
+    let
+      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
+      val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
+      val fields' = map (apsnd subst) fields;
+      val extension' = apsnd (map subst) extension;
+    in make_parent_info name fields' extension' ext_def induct_scheme end);
+
+end;
 
 
 
@@ -2415,7 +2428,7 @@
       handle ERROR msg =>
         cat_error msg ("The error(s) above occurred in parent record specification");
     val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
-    val parents = add_parents thy parent [];
+    val parents = get_parent_info thy parent;
 
     val bfields = map (prep_field cert_typ) raw_fields;