record package: corrected sort handling in type translations to avoid crashes when default sort is changed.
authorkrauss
Wed, 14 Apr 2010 16:15:19 +0200
changeset 36137 0be811a98d3a
parent 36134 c210a8fda4c5
child 36138 1faa0fc34174
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 *)
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