Changes

Summary

1. proper Thm.transfer;
2. clarified context: avoid capture of thy2 within closure;
3. tuned names;
4. more informative exceptions;
5. more permissive: allow collapse of term variables for equal results, e.g. relevant for metis (line 1882 of "~~/src/HOL/List.thy");
6. tuned;
7. more informative exception;
8. clarified signature;
9. clarified ML toplevel output: avoid "??." prefix;
10. tuned;