diff -r dbb8decc36bc -r c17fd2df4e9e src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Tue Nov 07 11:47:56 2006 +0100
+++ b/src/CTT/Arith.thy	Tue Nov 07 11:47:57 2006 +0100
@@ -32,10 +32,10 @@
   "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
 
 
-const_syntax (xsymbols)
+notation (xsymbols)
   mult  (infixr "#\<times>" 70)
 
-const_syntax (HTML output)
+notation (HTML output)
   mult (infixr "#\<times>" 70)