src/HOLCF/Pcpodef.thy

--- a/src/HOLCF/Pcpodef.thy	Mon Sep 01 22:10:42 2008 +0200
+++ b/src/HOLCF/Pcpodef.thy	Tue Sep 02 12:07:34 2008 +0200
@@ -17,8 +17,10 @@
   if the ordering is defined in the standard way.
 *}
 
+setup {* Sign.add_const_constraint (@{const_name Porder.sq_le}, NONE) *}
+
 theorem typedef_po:
-  fixes Abs :: "'a::po \<Rightarrow> 'b::sq_ord"
+  fixes Abs :: "'a::po \<Rightarrow> 'b::type"
   assumes type: "type_definition Rep Abs A"
     and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
   shows "OFCLASS('b, po_class)"
@@ -29,6 +31,9 @@
  apply (erule (1) antisym_less)
 done
 
+setup {* Sign.add_const_constraint (@{const_name Porder.sq_le},
+  SOME @{typ "'a::sq_ord \<Rightarrow> 'a::sq_ord \<Rightarrow> bool"}) *}
+
 subsection {* Proving a subtype is finite *}
 
 lemma typedef_finite_UNIV: