diff -r 26fefde1d124 -r d1064fa29424 Quot/Examples/FSet.thy
--- a/Quot/Examples/FSet.thy	Tue Dec 22 21:16:11 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 22 21:31:44 2009 +0100
@@ -43,7 +43,7 @@
 *}
 
 ML {*
-get_fun absF @{context} (@{typ "'a list"}, 
+absrep_fun absF @{context} (@{typ "'a list"}, 
                          @{typ "'a fset"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}
@@ -54,7 +54,7 @@
 term "abs_fset o (map id)"
 
 ML {*
-get_fun absF @{context} (@{typ "(nat * nat) list"}, 
+absrep_fun absF @{context} (@{typ "(nat * nat) list"}, 
                          @{typ "int fset"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}
@@ -66,7 +66,7 @@
 
 
 ML {*
-get_fun absF @{context} (@{typ "('a list) list"}, 
+absrep_fun absF @{context} (@{typ "('a list) list"}, 
                          @{typ "('a fset) fset"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}
@@ -74,7 +74,7 @@
 *}
 
 ML {*
-get_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 
+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}