src/Pure/Thy/thm_deps.ML
changeset 36744 6e1f3d609a68
parent 33769 6d8630fab26a
child 37216 3165bc303f66
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Sat May 08 17:10:27 2010 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat May 08 16:53:53 2010 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4        else
     1.5          let val {concealed, group, ...} = Name_Space.the_entry space name in
     1.6            fold_rev (fn th =>
     1.7 -            (case Thm.get_name th of
     1.8 +            (case Thm.derivation_name th of
     1.9                "" => I
    1.10              | a => cons (a, (th, concealed, group)))) ths
    1.11          end;