equal
deleted
inserted
replaced
54 in thm_of_atom thm Ts end |
54 in thm_of_atom thm Ts end |
55 |
55 |
56 | thm_of _ _ (PAxm (name, _, SOME Ts)) = |
56 | thm_of _ _ (PAxm (name, _, SOME Ts)) = |
57 thm_of_atom (Thm.axiom thy name) Ts |
57 thm_of_atom (Thm.axiom thy name) Ts |
58 |
58 |
59 | thm_of _ Hs (PBound i) = List.nth (Hs, i) |
59 | thm_of _ Hs (PBound i) = nth Hs i |
60 |
60 |
61 | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = |
61 | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) = |
62 let |
62 let |
63 val ([x], names') = Name.variants [s] names; |
63 val ([x], names') = Name.variants [s] names; |
64 val thm = thm_of ((x, T) :: vs, names') Hs prf |
64 val thm = thm_of ((x, T) :: vs, names') Hs prf |