changeset 41489 | 8e2b8649507d |
parent 39557 | fe5722fce758 |
child 41565 | 9718c32f9c4e |
--- a/src/Pure/Thy/thm_deps.ML Mon Jan 10 08:18:49 2011 +0100 +++ b/src/Pure/Thy/thm_deps.ML Mon Jan 10 15:19:48 2011 +0100 @@ -20,7 +20,7 @@ fun add_dep ("", _, _) = I | add_dep (name, _, PBody {thms = thms', ...}) = let - val prefix = #1 (Library.split_last (Long_Name.explode name)); + val prefix = #1 (split_last (Long_Name.explode name)); val session = (case prefix of a :: _ =>