# HG changeset patch
# User huffman
# Date 1323348364 -3600
# Node ID 9049b24959ded14793a9db730b33ba6a92e4eddf
# Parent  9fcaf2557c59df911e0864195c1f80191a3cb50c
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort

diff -r 9fcaf2557c59 -r 9049b24959de src/HOL/HOLCF/ex/Letrec.thy
--- a/src/HOL/HOLCF/ex/Letrec.thy	Thu Dec 08 13:25:54 2011 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Thu Dec 08 13:46:04 2011 +0100
@@ -8,10 +8,8 @@
 imports HOLCF
 begin
 
-default_sort pcpo
-
 definition
-  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
+  CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where
   "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
 
 nonterminal recbinds and recbindt and recbind