# HG changeset patch
# User wenzelm
# Date 1183586776 -7200
# Node ID 5ca3b23c09edcee9cd46cfccd8e862b984976f2e
# Parent  c5b93c69afd3833b05f30404ac33dbdb9ec67300
avoid polymorphic equality;
removed dead code;

diff -r c5b93c69afd3 -r 5ca3b23c09ed src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Jul 05 00:06:14 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Jul 05 00:06:16 2007 +0200
@@ -513,7 +513,7 @@
 
 fun decode_type thy t =
   let
-    fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy);
+    fun get_sort xs n = AList.lookup (op =) xs (n: indexname) |> the_default (Sign.defaultS thy);
     val map_sort = Sign.intern_sort thy;
   in
     Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
@@ -739,8 +739,6 @@
       (* tm is term representation of a (nested) field type. We first reconstruct the      *)
       (* type from tm so that we can continue on the type level rather then the term level.*)
 
-      fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy);
-
       (* WORKAROUND:
        * If a record type occurs in an error message of type inference there
        * may be some internal frees donoted by ??:
@@ -787,7 +785,6 @@
 fun record_type_tr' sep mark record record_scheme ctxt t =
   let
     val thy = ProofContext.theory_of ctxt;
-    fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy);
 
     val T = decode_type thy t;
     val varifyT = varifyT (Term.maxidx_of_typ T);