--- a/src/HOL/Induct/Comb.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Induct/Comb.thy Tue Nov 07 11:47:57 2006 +0100 @@ -25,7 +25,7 @@ | S | Ap comb comb (infixl "##" 90) -const_syntax (xsymbols) +notation (xsymbols) Ap (infixl "\<bullet>" 90)