
diff -r 4adf25becaa4 -r 4078d5e8b293 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jul 13 23:08:20 2000 +0200
+++ b/src/HOL/Fun.thy	Thu Jul 13 23:08:42 2000 +0200
@@ -81,7 +81,7 @@
   Applyall :: "[('a => 'b) set, 'a]=> 'b set"
     "Applyall F a == (%f. f a) `` F"
 
-  compose :: "['a set, 'a => 'b, 'b => 'c] => ('a => 'c)"
+  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
     "compose A g f == lam x : A. g(f x)"
 
   Inv    :: "['a set, 'a => 'b] => ('b => 'a)"




