# HG changeset patch # User schirmer # Date 1115997544 -7200 # Node ID f2a0a80d82334be38b957f665bad582021b15ac8 # Parent 0da64b5a9a00a5b73e668669ce382bb25271535a Bugfix in syntax translation for record type. diff -r 0da64b5a9a00 -r f2a0a80d8233 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu May 12 18:24:42 2005 +0200 +++ b/src/HOL/Tools/record_package.ML Fri May 13 17:19:04 2005 +0200 @@ -43,7 +43,7 @@ end; -structure RecordPackage:RECORD_PACKAGE = +structure RecordPackage:RECORD_PACKAGE = struct val rec_UNIV_I = thm "rec_UNIV_I"; @@ -567,10 +567,12 @@ fun get_sort xs n = (case assoc (xs,n) of SOME s => s | NONE => Sign.defaultS sg); - fun to_type t = Sign.intern_typ sg - (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t); + val tsig = Sign.tsig_of sg; + fun to_type t = Type.cert_typ tsig + (Sign.intern_typ sg + (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)); fun unify (t,env) = Type.unify tsig env t; fun mk_ext (fargs as (name,arg)::_) =