equal
deleted
inserted
replaced
18 fun thm_deps thy thms = |
18 fun thm_deps thy thms = |
19 let |
19 let |
20 fun add_dep ("", _, _) = I |
20 fun add_dep ("", _, _) = I |
21 | add_dep (name, _, PBody {thms = thms', ...}) = |
21 | add_dep (name, _, PBody {thms = thms', ...}) = |
22 let |
22 let |
23 val prefix = #1 (Library.split_last (Long_Name.explode name)); |
23 val prefix = #1 (split_last (Long_Name.explode name)); |
24 val session = |
24 val session = |
25 (case prefix of |
25 (case prefix of |
26 a :: _ => |
26 a :: _ => |
27 (case try (Context.get_theory thy) a of |
27 (case try (Context.get_theory thy) a of |
28 SOME thy => |
28 SOME thy => |