changeset 1970 | 90758c187861 |
parent 1969 | 9ae5380c828a |
child 1971 | 8daf6ff5e11a |
--- a/Nominal/NewFv.thy Wed Apr 28 07:20:57 2010 +0200 +++ b/Nominal/NewFv.thy Wed Apr 28 07:27:28 2010 +0200 @@ -26,7 +26,7 @@ ML {* fun is_atom thy ty = - Sign.of_sort thy (ty, @{sort at}) + Sign.of_sort thy (ty, @{sort at_base}) fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t | is_atom_set _ _ = false;