# HG changeset patch
# User wenzelm
# Date 997285133 -7200
# Node ID 1fd5469c195e31281d936d48dd27ac411d2ca27a
# Parent  4ff900551340ab0221bb5c03a5ac8e3a18806f5e
_constify;

diff -r 4ff900551340 -r 1fd5469c195e src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Aug 08 17:38:29 2001 +0200
+++ b/src/HOL/Record.thy	Wed Aug 08 17:38:53 2001 +0200
@@ -17,8 +17,8 @@
 
 syntax
   (*field names*)
-  "_field_name"         :: "id => ident"                                ("_")
-  "_field_name"         :: "longid => ident"                            ("_")
+  "_constify"           :: "id => ident"                                ("_")
+  "_constify"           :: "longid => ident"                            ("_")
 
   (*record types*)
   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")