changeset 28375 | c879d88d038a |
parent 28103 | b79e61861f0f |
child 28443 | de653f1ad78b |
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Sep 26 17:24:15 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Sep 26 19:07:56 2008 +0200 @@ -613,7 +613,7 @@ val ctx = Toplevel.context_of (Isar.state ()) (* NB: raises UNDEF *) val thy = Context.theory_of_proof ctx val ths = [PureThy.get_thm thy thmname] - val deps = filter_out (equal "") + val deps = filter_out (fn s => s = "") (Symtab.keys (fold Proofterm.thms_of_proof (map Thm.proof_of ths) Symtab.empty)) in