1.1 --- a/src/HOL/Tools/record.ML	Sat Jan 15 15:37:49 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Jan 15 16:49:10 2011 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4      cases: thm, simps: thm list, iffs: thm list}
     1.5    val get_info: theory -> string -> info option
     1.6    val the_info: theory -> string -> info
     1.7 +  val get_hierarchy: theory -> (string * typ list) -> (string * (string * typ) list) list
     1.8    val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
     1.9      (binding * typ * mixfix) list -> theory -> theory
    1.10  
    1.11 @@ -614,12 +615,14 @@
    1.12  
    1.13  (* parent records *)
    1.14  
    1.15 -fun add_parents _ NONE parents = parents
    1.16 -  | add_parents thy (SOME (types, name)) parents =
    1.17 +local
    1.18 +
    1.19 +fun add_parents _ NONE = I
    1.20 +  | add_parents thy (SOME (types, name)) =
    1.21        let
    1.22          fun err msg = error (msg ^ " parent record " ^ quote name);
    1.23  
    1.24 -        val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
    1.25 +        val {args, parent, ...} =
    1.26            (case get_info thy name of SOME info => info | NONE => err "Unknown");
    1.27          val _ = if length types <> length args then err "Bad number of arguments for" else ();
    1.28  
    1.29 @@ -631,12 +634,22 @@
    1.30          val inst = map fst args ~~ types;
    1.31          val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
    1.32          val parent' = Option.map (apfst (map subst)) parent;
    1.33 -        val fields' = map (apsnd subst) fields;
    1.34 -        val extension' = apsnd (map subst) extension;
    1.35 -      in
    1.36 -        add_parents thy parent'
    1.37 -          (make_parent_info name fields' extension' ext_def induct_scheme :: parents)
    1.38 -      end;
    1.39 +      in cons (name, inst) #> add_parents thy parent' end;
    1.40 +
    1.41 +in
    1.42 +
    1.43 +fun get_hierarchy thy (name, types) = add_parents thy (SOME (types, name)) [];
    1.44 +
    1.45 +fun get_parent_info thy parent =
    1.46 +  add_parents thy parent [] |> map (fn (name, inst) =>
    1.47 +    let
    1.48 +      val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
    1.49 +      val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
    1.50 +      val fields' = map (apsnd subst) fields;
    1.51 +      val extension' = apsnd (map subst) extension;
    1.52 +    in make_parent_info name fields' extension' ext_def induct_scheme end);
    1.53 +
    1.54 +end;
    1.55  
    1.56  
    1.57  
    1.58 @@ -2415,7 +2428,7 @@
    1.59        handle ERROR msg =>
    1.60          cat_error msg ("The error(s) above occurred in parent record specification");
    1.61      val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []);
    1.62 -    val parents = add_parents thy parent [];
    1.63 +    val parents = get_parent_info thy parent;
    1.64  
    1.65      val bfields = map (prep_field cert_typ) raw_fields;
    1.66