equal
deleted
inserted
replaced
56 let val thm_id = Proofterm.thm_id (i, thm_node) in |
56 let val thm_id = Proofterm.thm_id (i, thm_node) in |
57 (case lookup thm_id of |
57 (case lookup thm_id of |
58 SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res |
58 SOME thm_name => Inttab.update (i, (thm_id, thm_name)) res |
59 | NONE => fold deps (Proofterm.thm_node_thms thm_node) res) |
59 | NONE => fold deps (Proofterm.thm_node_thms thm_node) res) |
60 end; |
60 end; |
61 in fn thm => fold deps (Thm.thm_deps thm) Inttab.empty |> Inttab.dest |> map #2 end; |
61 in |
|
62 fn thm => |
|
63 fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty |
|
64 |> Inttab.dest |> map #2 |
|
65 end; |
62 |
66 |
63 |
67 |
64 (* thm_deps_cmd *) |
68 (* thm_deps_cmd *) |
65 |
69 |
66 fun thm_deps_cmd thy thms = |
70 fun thm_deps_cmd thy thms = |