diff -r dbb8decc36bc -r c17fd2df4e9e src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Tue Nov 07 11:47:56 2006 +0100
+++ b/src/HOL/Lambda/Type.thy	Tue Nov 07 11:47:57 2006 +0100
@@ -15,10 +15,10 @@
   shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"    ("_<_:_>" [90, 0, 0] 91)
   "e<i:a> = (\<lambda>j. if j < i then e j else if j = i then a else e (j - 1))"
 
-const_syntax (xsymbols)
+notation (xsymbols)
   shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
 
-const_syntax (HTML output)
+notation (HTML output)
   shift  ("_\<langle>_:_\<rangle>" [90, 0, 0] 91)
 
 lemma shift_eq [simp]: "i = j \<Longrightarrow> (e\<langle>i:T\<rangle>) j = T"
@@ -60,10 +60,10 @@
     ("_ ||- _ : _" [50, 50, 50] 50)
   "env ||- ts : Ts == typings env ts Ts"
 
-const_syntax (xsymbols)
+notation (xsymbols)
   typing_rel  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
 
-const_syntax (latex)
+notation (latex)
   funs  (infixr "\<Rrightarrow>" 200)
   typings_rel  ("_ \<tturnstile> _ : _" [50, 50, 50] 50)