diff -r d1ab5d2d6926 -r 8ddf1330f2ed Nominal/FSet.thy
--- a/Nominal/FSet.thy	Sun Jun 13 20:54:50 2010 +0200
+++ b/Nominal/FSet.thy	Mon Jun 14 04:38:25 2010 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory FSet
-imports Quotient_List
+imports Quotient_List Quotient_Product
 begin
 
 text {* Definiton of List relation and the quotient type *}
@@ -1626,6 +1626,33 @@
 *}
 
 ML {*
+let
+val parser = Args.context -- Scan.lift Args.name_source
+fun typ_pat (ctxt, str) =
+str |> Syntax.parse_typ ctxt
+|> ML_Syntax.print_typ
+|> ML_Syntax.atomic
+in
+ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
+end
+*}
+
+ML {*
+  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
+  |> Syntax.check_term @{context}
+  |> fastype_of
+  |> Syntax.string_of_typ @{context}
+  |> warning
+*}
+
+ML {*
+  mk_mapfun @{context} [@{typ_pat "?'a"}] @{typ_pat "(?'a list) * nat"}
+  |> Syntax.check_term @{context}
+  |> Syntax.string_of_term @{context}
+  |> warning
+*}
+
+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