# 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)::_) =