src/HOLCF/Fun1.thy

--- a/src/HOLCF/Fun1.thy	Sat Dec 01 18:51:46 2001 +0100
+++ b/src/HOLCF/Fun1.thy	Sat Dec 01 18:52:32 2001 +0100
@@ -13,7 +13,7 @@
 instance flat<chfin (flat_imp_chfin)
 
 (* to make << defineable: *)
-instance fun  :: (term,sq_ord)sq_ord
+instance fun  :: (type, sq_ord) sq_ord
 
 defs
   less_fun_def "(op <<) == (%f1 f2.!x. f1 x << f2 x)"