--- 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}