Improve AbstractAtom case in check_judgement in eval

[anjapetkovic]

in src/runtime/eval.ml the function check_judgement in case of Syntax.AbstractAtom _ goes to infer mode and then checks the result. This could be improved, it would be something like Syntax.Sequence except that c1 will be required to be an atom. We also have to "shave off" one layer of abstraction to the boundary and check that the atom has the required type given by the abstraction in the boundary.