equal
deleted
inserted
replaced
55 fun lam [] = ([], cont_K) |
55 fun lam [] = ([], cont_K) |
56 | lam (x::ys) = |
56 | lam (x::ys) = |
57 let |
57 let |
58 (* should use "close_derivation" for thms that are used multiple times *) |
58 (* should use "close_derivation" for thms that are used multiple times *) |
59 (* it seems to allow for sharing in explicit proof objects *) |
59 (* it seems to allow for sharing in explicit proof objects *) |
60 val x' = Thm.close_derivation (k x) |
60 val x' = Thm.close_derivation \<^here> (k x) |
61 val Lx = x' RS cont_L |
61 val Lx = x' RS cont_L |
62 in (map (fn y => SOME (k y RS Lx)) ys, x') end |
62 in (map (fn y => SOME (k y RS Lx)) ys, x') end |
63 |
63 |
64 (* first list: cont thm for each dangling bound variable *) |
64 (* first list: cont thm for each dangling bound variable *) |
65 (* second list: cont thm for each LAM in t *) |
65 (* second list: cont thm for each LAM in t *) |