--- a/QuotMain.thy	Mon Oct 12 23:16:20 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 23:39:14 2009 +0200
@@ -166,7 +166,7 @@
 where
   r_eq: "EQUIV RR"
 
-quotient qtrm = "trm" / "RR"
+quotient qtrm = trm / "RR"
   apply(rule r_eq)
   done
 
@@ -196,7 +196,7 @@
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
-quotient "'a qtrm'" = "'a trm'" / "R'"
+quotient qtrm' = "'a trm'" / "R'"
   apply(rule r_eq')
   done
 
@@ -218,7 +218,7 @@
 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
 axioms t_eq: "EQUIV Rt"
 
-quotient "qt" = "t" / "Rt"
+quotient qt = "t" / "Rt"
   by (rule t_eq)
 
 section {* lifting of constants *}
@@ -408,7 +408,7 @@
 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
-quotient "'a qt'" = "'a t'" / "Rt'"
+quotient qt' = "'a t'" / "Rt'"
   apply(rule t_eq')
   done
 
@@ -453,7 +453,7 @@
   apply(auto intro: list_eq.intros list_eq_refl)
   done
 
-quotient "'a fset" = "'a list" / "list_eq"
+quotient fset = "'a list" / "list_eq"
   apply(rule equiv_list_eq)
   done