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