concrete syntax for all constructors, to workaround authentic syntax problem with domain package;

--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Sun Feb 21 21:11:44 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Sun Feb 21 21:12:26 2010 +0100
@@ -8,7 +8,7 @@
 imports HOLCF
 begin
 
-domain 'a seq = nil | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
+domain 'a seq = nil  ("nil") | cons (HD :: 'a) (lazy TL :: "'a seq")  (infixr "##" 65)
 
 consts
    sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"

--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Feb 21 21:11:44 2010 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Sun Feb 21 21:12:26 2010 +0100
@@ -40,7 +40,7 @@
   "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
 translations
   "[x, xs!]"     == "x>>[xs!]"
-  "[x!]"         == "x>>CONST nil"
+  "[x!]"         == "x>>nil"
   "[x, xs?]"     == "x>>[xs?]"
   "[x?]"         == "x>>CONST UU"