src/HOL/Import/shuffler.ML
changeset 36692 54b64d4ad524
parent 36614 b6c031ad3690
child 36945 9bec62c10714
     1.1 --- a/src/HOL/Import/shuffler.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -550,7 +550,7 @@
     1.4  fun match_consts ignore t (* th *) =
     1.5      let
     1.6          fun add_consts (Const (c, _), cs) =
     1.7 -            if c mem_string ignore
     1.8 +            if member (op =) ignore c
     1.9              then cs
    1.10              else insert (op =) c cs
    1.11            | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))