Nominal/Fv.thy
changeset 1362 e72d9d9eada3
parent 1359 3bf496a971c6
child 1366 2bf82fa871e7
--- 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 _ [] [] = []