1.1 --- a/src/HOL/Predicate.thy	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -221,11 +221,11 @@
     1.4  subsubsection {* Composition  *}
     1.5  
     1.6  inductive
     1.7 -  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
     1.8 +  pred_comp  :: "['a => 'b => bool, 'b => 'c => bool] => 'a => 'c => bool"
     1.9      (infixr "OO" 75)
    1.10 -  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
    1.11 +  for r :: "'a => 'b => bool" and s :: "'b => 'c => bool"
    1.12  where
    1.13 -  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
    1.14 +  pred_compI [intro]: "r a b ==> s b c ==> (r OO s) a c"
    1.15  
    1.16  inductive_cases pred_compE [elim!]: "(r OO s) a c"
    1.17