src/HOLCF/ex/Pattern_Match.thy
changeset 40329 73f2b99b549d
parent 40327 1dfdbd66093a
child 40735 6f65843e78f3
--- a/src/HOLCF/ex/Pattern_Match.thy	Sat Oct 30 12:25:18 2010 -0700
+++ b/src/HOLCF/ex/Pattern_Match.thy	Sat Oct 30 15:13:11 2010 -0700
@@ -8,6 +8,8 @@
 imports HOLCF
 begin
 
+default_sort pcpo
+
 text {* FIXME: Find a proper way to un-hide constants. *}
 
 abbreviation fail :: "'a match"