changeset 27865 | 27a8ad9612a3 |
parent 27860 | 5125b3c1efc2 |
child 28020 | 1ff5167592ba |
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Aug 14 16:52:46 2008 +0200 @@ -176,7 +176,7 @@ fun tell_thm_deps ths = if print_mode_active thm_depsN then let - val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); + val names = map Thm.get_name_hint (filter Thm.has_name_hint ths); val deps = Symtab.keys (fold Proofterm.thms_of_proof' (map Thm.proof_of ths) Symtab.empty); in