# HG changeset patch
# User wenzelm
# Date 997285156 -7200
# Node ID f9ae28f55178964fc726cae0bbeb976f5dbe09d7
# Parent  1fd5469c195e31281d936d48dd27ac411d2ca27a
field_name_ast_tr superceded by constify_ast_tr in Pure;

diff -r 1fd5469c195e -r f9ae28f55178 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Aug 08 17:38:53 2001 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Aug 08 17:39:16 2001 +0200
@@ -223,16 +223,6 @@
 
 (** 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, _) $ Const (name, _) $ arg) =
@@ -975,7 +965,7 @@
 
 val setup =
  [RecordsData.init,
-  Theory.add_trfuns (parse_ast_translation, parse_translation, [], []),
+  Theory.add_trfuns ([], parse_translation, [], []),
   Method.add_methods [record_split_method],
   Simplifier.change_simpset_of Simplifier.addsimprocs [record_simproc]];