Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/record.ML
changeset 36137 0be811a98d3a
parent 35994 9cc3df9a606e
child 36151 b89a2a05a3ce 
--- 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
isabelle