--- a/Quot/Examples/FSet.thy	Tue Dec 22 22:10:48 2009 +0100
+++ b/Quot/Examples/FSet.thy	Wed Dec 23 10:31:54 2009 +0100
@@ -26,61 +26,6 @@
   fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
-
-fun
-  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
-  "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
-  apply(unfold equivp_def)
-  apply(auto simp add: mem_def expand_fun_eq)
-  done
-
-
-ML {*
-open Quotient_Term;
-*}
-
-ML {*
-absrep_fun absF @{context} (@{typ "'a list"}, 
-                         @{typ "'a fset"})
-|> Syntax.check_term @{context}
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-term "map id"
-term "abs_fset o (map id)"
-
-ML {*
-absrep_fun absF @{context} (@{typ "(nat * nat) list"}, 
-                         @{typ "int fset"})
-|> Syntax.check_term @{context}
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-term "map abs_int"
-term "abs_fset o map abs_int"
-
-
-ML {*
-absrep_fun absF @{context} (@{typ "('a list) list"}, 
-                         @{typ "('a fset) fset"})
-|> Syntax.check_term @{context}
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
-ML {*
-absrep_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 
-                         @{typ "('a fset) fset \<Rightarrow> 'a"})
-|> Syntax.check_term @{context}
-|> Syntax.string_of_term @{context}
-|> writeln
-*}
-
 quotient_definition
    "EMPTY :: 'a fset"
 as