author | clasohm |
Fri, 09 Feb 1996 12:18:02 +0100 | |
changeset 1484 | b43cd8a8061f |
parent 1483 | 617ca7312ceb |
child 1485 | 240cc98b94a7 |
src/Pure/type.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/type.ML Thu Feb 08 12:26:16 1996 +0100 +++ b/src/Pure/type.ML Fri Feb 09 12:18:02 1996 +0100 @@ -333,9 +333,9 @@ fun inst_term_tvars(tsig, tye) = map_term_types (inst_typ_tvars(tsig, tye)); -(* expand_typ *) +(* norm_typ *) -fun expand_typ (TySg {abbrs, ...}) ty = +fun norm_typ (TySg {abbrs, ...}) ty = let val idx = maxidx_of_typ ty + 1; @@ -349,9 +349,6 @@ expand ty end; -val norm_typ = expand_typ; - - (** type matching **)