# HG changeset patch
# User wenzelm
# Date 1266783146 -3600
# Node ID afbb9cc4a7dbceecc212e90fca6ede34de625162
# Parent  8154c5211ddb44f0d6c4cf1073ffb454ac748f87
concrete syntax for all constructors, to workaround authentic syntax problem with domain package;

diff -r 8154c5211ddb -r afbb9cc4a7db src/HOLCF/IOA/meta_theory/Seq.thy
--- 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"
diff -r 8154c5211ddb -r afbb9cc4a7db src/HOLCF/IOA/meta_theory/Sequence.thy
--- 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"