--- a/src/HOL/Record.thy Fri Jun 12 17:05:04 1998 +0200
+++ b/src/HOL/Record.thy Fri Jun 12 17:06:14 1998 +0200
@@ -20,8 +20,8 @@
"_field" :: "[ident, 'a] => field" ("(2_ =/ _)")
"" :: "field => fields" ("_")
"_fields" :: "[field, fields] => fields" ("_,/ _")
- "_record" :: "fields => 'a" ("({: _ :})")
- "_record_scheme" :: "[fields, 'a] => 'b" ("({: _,/ (2... =/ _) :})")
+ "_record" :: "fields => 'a" ("('(| _ |'))")
+ "_record_scheme" :: "[fields, 'a] => 'b" ("('(| _,/ (2... =/ _) |'))")
(* type class for record extensions *)