# HG changeset patch
# User wenzelm
# Date 1267045161 -3600
# Node ID 1391f82da5a4c391443e433eedf2414ef52f7d0e
# Parent  fa051b504c3f8b8555e920922c7584d692de1619
proper type syntax (cf. 7425aece4ee3);

diff -r fa051b504c3f -r 1391f82da5a4 src/HOL/Nominal/Nominal.thy
--- 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 *}
 (*===================================================*)