diff -r fe6eb116b341 -r c55883442514 FSet.thy
--- a/FSet.thy	Tue Nov 03 17:30:27 2009 +0100
+++ b/FSet.thy	Tue Nov 03 17:30:43 2009 +0100
@@ -34,7 +34,7 @@
 thm "Rep_fset"
 thm "ABS_fset_def"
 
-quotient_def (for "'a fset")
+quotient_def 
   EMPTY :: "'a fset"
 where
   "EMPTY \<equiv> ([]::'a list)"
@@ -43,7 +43,7 @@
 term EMPTY
 thm EMPTY_def
 
-quotient_def (for "'a fset")
+quotient_def 
   INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "INSERT \<equiv> op #"
@@ -52,7 +52,7 @@
 term INSERT
 thm INSERT_def
 
-quotient_def (for "'a fset")
+quotient_def 
   FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "FUNION \<equiv> (op @)"
@@ -78,7 +78,7 @@
   card1_nil: "(card1 []) = 0"
 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))"
 
-quotient_def (for "'a fset")
+quotient_def 
   CARD :: "'a fset \<Rightarrow> nat"
 where
   "CARD \<equiv> card1"
@@ -144,7 +144,7 @@
   apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1)
   done
 
-quotient_def (for "'a fset")
+quotient_def 
   IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 where
   "IN \<equiv> membship"
@@ -168,7 +168,7 @@
 thm fold_def
 
 (* FIXME: does not work yet for all types*)
-quotient_def (for "'a fset" "'b fset")
+quotient_def 
   fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
   "fmap \<equiv> map"