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