# HG changeset patch
# User schirmer
# Date 1083662642 -7200
# Node ID 62a724ce51c7b818257c9d6c902b9f407b8c72df
# Parent  2f885b7e5ba725e1721b28e0c2e4e167d42f38d7
tuned;

diff -r 2f885b7e5ba7 -r 62a724ce51c7 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon May 03 23:22:17 2004 +0200
+++ b/src/HOL/Record.thy	Tue May 04 11:24:02 2004 +0200
@@ -56,25 +56,6 @@
   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
 
-(* 
-
-  "_structure"             :: "fields => 'a"          ("(3{| _ |})")
-  "_structure_scheme"      :: "[fields, 'a] => 'a"    ("(3{| _,/ (2... =/ _) |})")
-  
-  "_structure_update_name":: idt
-  "_structure_update"  :: "['a, updates] \<Rightarrow> 'b"    ("_/(3{| _ |})" [900,0] 900)
-
-  "_structure_type"        :: "field_types => type"    ("(3{| _ |})")
-  "_structure_type_scheme" :: "[field_types, type] => type" 
-                                      ("(3{| _,/ (2... ::/ _) |})")
-syntax (xsymbols)
-
- "_structure_scheme"   :: "[fields, 'a] => 'a"       ("(3{|_,/ (2\<dots> =/ _)|})")
-
-  "_structure_type_scheme" :: "[field_types, type] => type"        
-                                      ("(3{|_,/ (2\<dots> ::/ _)|})")
-
-*)
 use "Tools/record_package.ML";
 setup RecordPackage.setup;