src/Pure/Thy/thm_deps.ML
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;