# HG changeset patch
# User wenzelm
# Date 997216650 -7200
# Node ID 4546d8d392213ecfceae8793631d8fd4e8943e3b
# Parent  d08d4e17a5f662246627517f9e891b48fc8d4585
fix problem with user translations by making field names appear as consts;

diff -r d08d4e17a5f6 -r 4546d8d39221 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Tue Aug 07 21:27:00 2001 +0200
+++ b/src/HOL/Record.thy	Tue Aug 07 22:37:30 2001 +0200
@@ -17,8 +17,8 @@
 
 syntax
   (*field names*)
-  ""                    :: "id => ident"                                ("_")
-  ""                    :: "longid => ident"                            ("_")
+  "_field_name"         :: "id => ident"                                ("_")
+  "_field_name"         :: "longid => ident"                            ("_")
 
   (*record types*)
   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
diff -r d08d4e17a5f6 -r 4546d8d39221 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Aug 07 21:27:00 2001 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Aug 07 22:37:30 2001 +0200
@@ -223,9 +223,19 @@
 
 (** concrete syntax for records **)
 
+(* parse ast translations *)
+
+fun field_name_ast_tr [Syntax.Variable c] = Syntax.Constant c
+  | field_name_ast_tr asts = raise Syntax.AST ("field_name_ast_tr", asts);
+
+
+val parse_ast_translation =
+ [("_field_name", field_name_ast_tr)];
+
+
 (* parse translations *)
 
-fun gen_field_tr mark sfx (t as Const (c, _) $ Free (name, _) $ arg) =
+fun gen_field_tr mark sfx (t as Const (c, _) $ Const (name, _) $ arg) =
       if c = mark then Syntax.const (suffix sfx name) $ arg
       else raise TERM ("gen_field_tr: " ^ mark, [t])
   | gen_field_tr mark _ t = raise TERM ("gen_field_tr: " ^ mark, [t]);
@@ -965,7 +975,7 @@
 
 val setup =
  [RecordsData.init,
-  Theory.add_trfuns ([], parse_translation, [], []),
+  Theory.add_trfuns (parse_ast_translation, parse_translation, [], []),
   Method.add_methods [record_split_method],
   Simplifier.change_simpset_of Simplifier.addsimprocs [record_simproc]];