diff -r 93c9022ba5e9 -r c4001cda9da3 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -194,9 +194,9 @@
   done
 
 quotient_definition
-   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
-as
-   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
+  "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs"
+is
+  "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
 lemma [quot_respect]:
   shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"
@@ -234,7 +234,7 @@
 
 quotient_definition
   "permute_abs::perm \<Rightarrow> ('a::pt abs) \<Rightarrow> 'a abs"
-as
+is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
 lemma permute_ABS [simp]:
@@ -252,7 +252,7 @@
 
 quotient_definition
   "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool"
-as
+is
   "supp_abs_fun"
 
 lemma supp_Abs_fun_simp: