src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36692 54b64d4ad524
parent 36556 81dc2c20f052
child 36966 adc11fb3f3aa
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4    | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
     1.5        arity_clause dfg seen n (tcons,ars)
     1.6    | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
     1.7 -      if class mem_string seen then (*multiple arities for the same tycon, class pair*)
     1.8 +      if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
     1.9            make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
    1.10            arity_clause dfg seen (n+1) (tcons,ars)
    1.11        else