diff -r cd2aca704279 -r c9f71476b030 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Oct 19 10:10:41 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue Oct 19 15:08:24 2010 +0100
@@ -28,12 +28,12 @@
   fun_map ("_ \<singlearr> _" 51) and
   fun_rel ("_ \<doublearr> _" 51) and
   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
-  fempty ("\<emptyset>") and
-  funion ("_ \<union> _") and
-  finsert ("{_} \<union> _") and 
+  empty_fset ("\<emptyset>") and
+  union_fset ("_ \<union> _") and
+  insert_fset ("{_} \<union> _") and 
   Cons ("_::_") and
   concat ("flat") and
-  fconcat ("\<Union>") and
+  concat_fset ("\<Union>") and
   Quotient ("Quot _ _ _")
 
   
@@ -267,8 +267,8 @@
   builds finite unions of finite sets:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm fconcat_empty[THEN eq_reflection, no_vars]}\hspace{10mm} 
-  @{thm fconcat_insert[THEN eq_reflection, no_vars]}
+  @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm} 
+  @{thm concat_insert_fset[THEN eq_reflection, no_vars]}
   \end{isabelle}
 
   \noindent
@@ -377,10 +377,13 @@
   Using extensionality and unfolding the definition of @{text "\<singlearr>"}, 
   we can get back to \eqref{adddef}. 
   In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function 
-  of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
-  type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. 
-  For example @{text "map_list"}
-  has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
+  of the type-constructor @{text \<kappa>}. 
+  %% a general type for map all types is difficult to give (algebraic types are
+  %% easy, but for example the function type is not algebraic
+  %For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
+  %type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. 
+  %For example @{text "map_list"}
+  %has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
   In our implementation we maintain
   a database of these map-functions that can be dynamically extended.