equal
deleted
inserted
replaced
45 |
45 |
46 (*--------------------------------------------------------------------------- |
46 (*--------------------------------------------------------------------------- |
47 * Typing |
47 * Typing |
48 *---------------------------------------------------------------------------*) |
48 *---------------------------------------------------------------------------*) |
49 |
49 |
50 fun typecheck thry t = |
50 fun typecheck thy t = |
51 Thm.global_cterm_of thry t |
51 Thm.global_cterm_of thy t |
52 handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg |
52 handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg |
53 | TERM (msg, _) => raise THRY_ERR "typecheck" msg; |
53 | TERM (msg, _) => raise THRY_ERR "typecheck" msg; |
54 |
54 |
55 |
55 |
56 (*--------------------------------------------------------------------------- |
56 (*--------------------------------------------------------------------------- |