diff -r d835a2771608 -r e9b0728061a8 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Tue Jun 22 13:05:00 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jun 22 13:31:42 2010 +0100
@@ -65,6 +65,10 @@
   Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
 end
 
+
+fun dest_fsetT (Type (@{type_name fset}, [T])) = T
+  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+
 fun mk_atom_fset t =
 let
   val ty = fastype_of t;