# HG changeset patch
# User huffman
# Date 1269324163 25200
# Node ID 9c59c490c4e553b60a639211002b026796fe1146
# Parent  bfa52a972745326a1dadf833467fa4bcf31260eb
define CLetrec using Pair, fst, snd instead of cpair, cfst, csnd

diff -r bfa52a972745 -r 9c59c490c4e5 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Mon Mar 22 22:55:26 2010 -0700
+++ b/src/HOLCF/Fix.thy	Mon Mar 22 23:02:43 2010 -0700
@@ -207,7 +207,7 @@
 
 definition
   CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
-  "CLetrec = (\<Lambda> F. csnd\<cdot>(F\<cdot>(\<mu> x. cfst\<cdot>(F\<cdot>x))))"
+  "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
 
 nonterminals
   recbinds recbindt recbind
@@ -221,13 +221,13 @@
   "_Letrec"   :: "[recbinds, 'a] \<Rightarrow> 'a"      ("(Letrec (_)/ in (_))" 10)
 
 translations
-  (recbindt) "x = a, \<langle>y,ys\<rangle> = \<langle>b,bs\<rangle>" == (recbindt) "\<langle>x,y,ys\<rangle> = \<langle>a,b,bs\<rangle>"
-  (recbindt) "x = a, y = b"          == (recbindt) "\<langle>x,y\<rangle> = \<langle>a,b\<rangle>"
+  (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
+  (recbindt) "x = a, y = b"          == (recbindt) "(x,y) = (a,b)"
 
 translations
   "_Letrec (_recbinds b bs) e" == "_Letrec b (_Letrec bs e)"
-  "Letrec xs = a in \<langle>e,es\<rangle>"    == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e,es\<rangle>)"
-  "Letrec xs = a in e"         == "CONST CLetrec\<cdot>(\<Lambda> xs. \<langle>a,e\<rangle>)"
+  "Letrec xs = a in (e,es)"    == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e,es))"
+  "Letrec xs = a in e"         == "CONST CLetrec\<cdot>(\<Lambda> xs. (a,e))"
 
 text {*
   Bekic's Theorem: Simultaneous fixed points over pairs