# HG changeset patch
# User krauss
# Date 1271254519 -7200
# Node ID 0be811a98d3ab3cbedba2fbf057269cc8d834735
# Parent  c210a8fda4c5a0c5c904377a643d498265c472f8
record package: corrected sort handling in type translations to avoid crashes when default sort is changed.
Test case:
  record 'a T = elem :: 'a
  defaultsort order
  term elem (* low-level exception *)

diff -r c210a8fda4c5 -r 0be811a98d3a src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Apr 14 11:24:31 2010 +0200
+++ b/src/HOL/Tools/record.ML	Wed Apr 14 16:15:19 2010 +0200
@@ -901,7 +901,7 @@
     val varifyT = varifyT midx;
 
     fun mk_type_abbr subst name alphas =
-      let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
+      let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in
         Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
       end;
 
@@ -912,7 +912,7 @@
         SOME (name, _) =>
           if name = last_ext then
             let val subst = match schemeT T in
-              if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
+              if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS))))
               then mk_type_abbr subst abbr alphas
               else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
             end handle Type.TYPE_MATCH => record_type_tr' ctxt tm