diff -r cbd32a0f2f41 -r 74be52691d62 src/HOLCF/Fun2.thy
--- a/src/HOLCF/Fun2.thy	Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Fun2.thy	Thu Jun 29 16:28:40 1995 +0200
@@ -24,7 +24,8 @@
 
 inst_fun_po	"((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
 
-(* definitions *)
+defs
+
 (* The least element in type 'a::term => 'b::pcpo *)
 
 UU_fun_def	"UU_fun == (% x.UU)"