src/Pure/ProofGeneral/pgip_input.ML
changeset 36692 54b64d4ad524
parent 29606 fedb8be05f24
child 38228 ada3ab6b9085
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -227,8 +227,8 @@
     1.4     (* We allow sending proper document markup too; we map it back to dostep   *)
     1.5     (* and strip out metainfo elements. Markup correctness isn't checked: this *)
     1.6     (* is a compatibility measure to make it easy for interfaces.              *)
     1.7 -   | x => if (x mem PgipMarkup.doc_markup_elements) then
     1.8 -              if (x mem PgipMarkup.doc_markup_elements_ignored) then
     1.9 +   | x => if member (op =) PgipMarkup.doc_markup_elements x then
    1.10 +              if member (op =) PgipMarkup.doc_markup_elements_ignored x then
    1.11                    raise NoAction
    1.12                else 
    1.13                    Dostep { text = xmltext data } (* could separate out Doitem too *)