proper type syntax (cf. 7425aece4ee3);

--- a/src/HOL/Nominal/Nominal.thy	Wed Feb 24 21:55:46 2010 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Feb 24 21:59:21 2010 +0100
@@ -3403,13 +3403,13 @@
   where
   ABS_in: "(abs_fun a x)\<in>ABS_set"
 
-typedef (ABS) ('x,'a) ABS = "ABS_set::('x\<Rightarrow>('a noption)) set"
+typedef (ABS) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+  "ABS_set::('x\<Rightarrow>('a noption)) set"
 proof 
   fix x::"'a" and a::"'x"
   show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
 qed
 
-syntax ABS :: "type \<Rightarrow> type \<Rightarrow> type" ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000)
 
 section {* lemmas for deciding permutation equations *}
 (*===================================================*)