src/Pure/ProofGeneral/proof_general_pgip.ML
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