src/Pure/Thy/thm_deps.ML
changeset 30364 577edc39b501
parent 30280 eb98b49ef835
child 31174 f1f1e9b53c81
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4      fun add_dep ("", _, _) = I
     1.5        | add_dep (name, _, PBody {thms = thms', ...}) =
     1.6            let
     1.7 -            val prefix = #1 (Library.split_last (NameSpace.explode name));
     1.8 +            val prefix = #1 (Library.split_last (Long_Name.explode name));
     1.9              val session =
    1.10                (case prefix of
    1.11                  a :: _ =>
    1.12 @@ -33,7 +33,7 @@
    1.13                 | _ => ["global"]);
    1.14              val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
    1.15              val entry =
    1.16 -              {name = NameSpace.base_name name,
    1.17 +              {name = Long_Name.base_name name,
    1.18                 ID = name,
    1.19                 dir = space_implode "/" (session @ prefix),
    1.20                 unfold = false,