diff -r 9ae5380c828a -r 90758c187861 Nominal/NewFv.thy --- 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;