equal
deleted
inserted
replaced
60 |
60 |
61 | thm_of _ Hs (PBound i) = List.nth (Hs, i) |
61 | thm_of _ Hs (PBound i) = List.nth (Hs, i) |
62 |
62 |
63 | thm_of vs Hs (Abst (s, SOME T, prf)) = |
63 | thm_of vs Hs (Abst (s, SOME T, prf)) = |
64 let |
64 let |
65 val x = variant (names @ map fst vs) s; |
65 val x = Name.variant (names @ map fst vs) s; |
66 val thm = thm_of ((x, T) :: vs) Hs prf |
66 val thm = thm_of ((x, T) :: vs) Hs prf |
67 in |
67 in |
68 Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm |
68 Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm |
69 end |
69 end |
70 |
70 |