--- 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]];