# HG changeset patch
# User huffman
# Date 1269325982 25200
# Node ID 384a31bd5425960b231cac2cb32ed1f461a6d7bd
# Parent  9c59c490c4e553b60a639211002b026796fe1146
use Pair instead of cpair

diff -r 9c59c490c4e5 -r 384a31bd5425 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Mar 22 23:02:43 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Mon Mar 22 23:33:02 2010 -0700
@@ -175,7 +175,7 @@
   szip_nil: "szip$nil$y=nil"
 | szip_cons_nil: "x~=UU ==> szip$(x##xs)$nil=UU"
 | szip_cons:
-    "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys"
+    "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = (x,y)##szip$xs$ys"
 
 lemma szip_UU1 [simp]: "szip$UU$y=UU"
 by fixrec_simp