diff -r d95f39448121 -r 54b64d4ad524 src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed May 05 18:25:34 2010 +0200
@@ -227,8 +227,8 @@
    (* We allow sending proper document markup too; we map it back to dostep   *)
    (* and strip out metainfo elements. Markup correctness isn't checked: this *)
    (* is a compatibility measure to make it easy for interfaces.              *)
-   | x => if (x mem PgipMarkup.doc_markup_elements) then
-              if (x mem PgipMarkup.doc_markup_elements_ignored) then
+   | x => if member (op =) PgipMarkup.doc_markup_elements x then
+              if member (op =) PgipMarkup.doc_markup_elements_ignored x then
                   raise NoAction
               else 
                   Dostep { text = xmltext data } (* could separate out Doitem too *)