--- 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')