diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/domain/theorems.ML	Sun May 25 11:07:52 1997 +0200
@@ -51,7 +51,7 @@
                                 cut_facts_tac prems 1,
                                 fast_tac HOL_cs 1]);
 
-val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
+val dist_eqI = prove_goal Porder.thy "~(x::'a::po) << y ==> x ~= y" (fn prems => [
                                 rtac rev_contrapos 1,
                                 etac (antisym_less_inverse RS conjunct1) 1,
                                 resolve_tac prems 1]);