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 _ [] [] = []