# HG changeset patch
# User wenzelm
# Date 897663974 -7200
# Node ID 0c9939c2ab5cc50dc0aaa8fcc1d965a39e2fe509
# Parent  e2280a1eadb27017da568ba147bd291b762f65f6
changed {: :} syntax to (| |);

diff -r e2280a1eadb2 -r 0c9939c2ab5c src/HOL/Record.thy
--- 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 *)