diff -r 1e811e3424f3 -r e72d9d9eada3 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Mon Mar 08 11:25:57 2010 +0100
+++ b/Nominal/Fv.thy	Mon Mar 08 14:31:04 2010 +0100
@@ -58,6 +58,12 @@
   body.
 *)
 
+ML {*
+fun is_atom thy typ =
+  Sign.of_sort thy (typ, @{sort at})
+*}
+
+
 (* Like map2, only if the second list is empty passes empty lists insted of error *)
 ML {*
 fun map2i _ [] [] = []