# HG changeset patch
# User kleing
# Date 1202894370 -3600
# Node ID d80a49f51b9462e439bf0d7bb7b246d15b6b87d0
# Parent  65585de05a66842a61b3c6efa09fb1de441eb85d
fixed record pretty printing

diff -r 65585de05a66 -r d80a49f51b94 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Feb 13 09:35:33 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Wed Feb 13 10:19:30 2008 +0100
@@ -731,7 +731,7 @@
 
 fun gen_record_tr' name =
   let val name_sfx = suffix extN name;
-      val unit = (fn Const ("Unity",_) => true | _ => false);
+      val unit = (fn Const (@{const_syntax "Product_Type.Unity"},_) => true | _ => false);
       fun tr' ctxt ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
                        (list_comb (Syntax.const name_sfx,ts))
   in (name_sfx,tr')