src/Pure/proof_general.ML
changeset 20664 ffbc5a57191a
parent 20642 cfe2b0803a51
child 20738 a965cad7d455
     1.1 --- a/src/Pure/proof_general.ML	Thu Sep 21 19:04:12 2006 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Thu Sep 21 19:04:20 2006 +0200
     1.3 @@ -867,7 +867,7 @@
     1.4                 and even if we did, we'd have to mess around here a whole lot more first
     1.5                 to pick out the terms from the syntax. *)
     1.6  
     1.7 -            if (name mem plain_items) then plain_item
     1.8 +            if member (op =) plain_items name then plain_item
     1.9              else case name of
    1.10                       "text"      => comment_item
    1.11                     | "text_raw"  => comment_item
    1.12 @@ -1460,9 +1460,9 @@
    1.13  
    1.14  local
    1.15  
    1.16 -val regexp_meta = explode ".*+?[]^$";
    1.17 +val regexp_meta = member (op =) (explode ".*+?[]^$");
    1.18  val regexp_quote =
    1.19 -  implode o map (fn c => if c mem_string regexp_meta then "\\\\" ^ c else c) o explode;
    1.20 +  implode o map (fn c => if regexp_meta c then "\\\\" ^ c else c) o explode;
    1.21  
    1.22  fun defconst name strs =
    1.23    "\n(defconst isar-keywords-" ^ name ^