diff -r bc4d107fb6dd -r 194ae2e0c193 src/HOLCF/Discrete0.ML
--- a/src/HOLCF/Discrete0.ML	Fri May 23 18:55:28 1997 +0200
+++ b/src/HOLCF/Discrete0.ML	Sun May 25 11:07:52 1997 +0200
@@ -6,17 +6,17 @@
 Proves that 'a discr is a po
 *)
 
-goalw thy [less_discr_def] "less (x::('a::term)discr) x";
+goalw thy [less_discr_def] "(x::('a::term)discr) << x";
 by (rtac refl 1);
 qed "less_discr_refl";
 
 goalw thy [less_discr_def]
-  "!!x. [| less (x::('a::term)discr) y; less y z |] ==> less x z";
+  "!!x. [| (x::('a::term)discr) << y; y << z |] ==> x <<  z";
 by (etac trans 1);
 by (assume_tac 1);
 qed "less_discr_trans";
 
 goalw thy [less_discr_def]
-  "!!x. [| less (x::('a::term)discr) y; less y x |] ==> x=y";
+  "!!x. [| (x::('a::term)discr) << y; y << x |] ==> x=y";
 by (assume_tac 1);
 qed "less_discr_antisym";