--- 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 *}
(*===================================================*)