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 *)
1.1 --- a/src/HOL/Tools/record.ML Wed Apr 14 11:24:31 2010 +0200
1.2 +++ b/src/HOL/Tools/record.ML Wed Apr 14 16:15:19 2010 +0200
1.3 @@ -901,7 +901,7 @@
1.4 val varifyT = varifyT midx;
1.5
1.6 fun mk_type_abbr subst name alphas =
1.7 - let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
1.8 + let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in
1.9 Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
1.10 end;
1.11
1.12 @@ -912,7 +912,7 @@
1.13 SOME (name, _) =>
1.14 if name = last_ext then
1.15 let val subst = match schemeT T in
1.16 - if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, Sign.defaultS thy))))
1.17 + if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS))))
1.18 then mk_type_abbr subst abbr alphas
1.19 else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta])
1.20 end handle Type.TYPE_MATCH => record_type_tr' ctxt tm