diff -r f84dc3b811e9 -r 8712391bbf3d src/HOL/Record.thy
--- a/src/HOL/Record.thy	Thu Oct 22 20:13:21 1998 +0200
+++ b/src/HOL/Record.thy	Thu Oct 22 20:15:26 1998 +0200
@@ -23,21 +23,21 @@
   "_field_type"         :: "[ident, type] => field_type"           	("(2_ ::/ _)")
   ""               	:: "field_type => field_types"              	("_")
   "_field_types"	:: "[field_type, field_types] => field_types"   ("_,/ _")
-  "_record_type"	:: "field_types => type"                   	("('(| _ |'))")
-  "_record_type_scheme"	:: "[field_types, type] => type"	("('(| _,/ (2... ::/ _) |'))")
+  "_record_type"	:: "field_types => type"                   	("(3'(| _ |'))")
+  "_record_type_scheme"	:: "[field_types, type] => type"	("(3'(| _,/ (2... ::/ _) |'))")
 
   (*records*)
   "_field"          	:: "[ident, 'a] => field"           		("(2_ =/ _)")
   ""                	:: "field => fields"                		("_")
   "_fields"         	:: "[field, fields] => fields"      		("_,/ _")
-  "_record"         	:: "fields => 'a"                   		("('(| _ |'))")
-  "_record_scheme"  	:: "[fields, 'a] => 'a"             	("('(| _,/ (2... =/ _) |'))")
+  "_record"         	:: "fields => 'a"                   		("(3'(| _ |'))")
+  "_record_scheme"  	:: "[fields, 'a] => 'a"             	("(3'(| _,/ (2... =/ _) |'))")
 
   (*record updates*)
   "_update"	    	:: "[ident, 'a] => update"           		("(2_ :=/ _)")
   ""                	:: "update => updates"               		("_")
   "_updates"        	:: "[update, updates] => updates"    		("_,/ _")
-  "_record_update"  	:: "['a, updates] => 'b"               	("_/('(| _ |'))" [900,0] 900)
+  "_record_update"  	:: "['a, updates] => 'b"               	("_/(3'(| _ |'))" [900,0] 900)
 
 
 (* type class for record extensions *)