diff -r 5e98b3f231a0 -r 084b2b7df98a Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Jun 14 10:14:39 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 11:51:34 2010 +0200
@@ -1642,7 +1642,7 @@
   |> Syntax.check_term @{context}
   |> fastype_of
   |> Syntax.string_of_typ @{context}
-  |> warning
+  |> tracing
 *}
 
 ML {*
@@ -1653,6 +1653,16 @@
 *}
 
 ML {*
+  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
+  |> Syntax.check_term @{context}
+*}
+
+term prod_fun
+term map
+term fun_map
+term "op o"
+
+ML {*
   absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
   |> Syntax.string_of_term @{context}
   |> writeln