# HG changeset patch
# User wenzelm
# Date 1295203499 -3600
# Node ID 484eedf607da2f0c9241671e5545b7b4089aea4f
# Parent  6eeda4b417b31b931ad2950aa89b56347239cc62
proper type variables with sorts;

diff -r 6eeda4b417b3 -r 484eedf607da src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Jan 16 17:01:49 2011 +0100
+++ b/src/HOL/Tools/record.ML	Sun Jan 16 19:44:59 2011 +0100
@@ -25,7 +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 get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
   val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
     (binding * typ * mixfix) list -> theory -> theory
 
@@ -631,8 +631,8 @@
         val bads = map_filter bad_inst (args ~~ types);
         val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
 
-        val inst = map fst args ~~ types;
-        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);
+        val inst = args ~~ types;
+        val subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
         val parent' = Option.map (apfst (map subst)) parent;
       in cons (name, inst) #> add_parents thy parent' end;
 
@@ -643,7 +643,7 @@
 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 subst = Term.map_type_tfree (the o AList.lookup (op =) inst);
       val {fields, extension, induct_scheme, ext_def, ...} = the_info thy name;
       val fields' = map (apsnd subst) fields;
       val extension' = apsnd (map subst) extension;