src/HOL/Tools/res_hol_clause.ML
changeset 33037 b22e44496dc2
parent 32994 ccc07fbbfefd
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4    | combterm_of dfg thy (P $ Q) =
     1.5        let val (P',tsP) = combterm_of dfg thy P
     1.6            val (Q',tsQ) = combterm_of dfg thy Q
     1.7 -      in  (CombApp(P',Q'), tsP union tsQ)  end
     1.8 +      in  (CombApp(P',Q'), gen_union (op =) (tsP, tsQ))  end
     1.9    | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t);
    1.10  
    1.11  fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
    1.12 @@ -166,7 +166,7 @@
    1.13    | literals_of_term1 dfg thy (lits,ts) P =
    1.14        let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
    1.15        in
    1.16 -          (Literal(pol,pred)::lits, ts union ts')
    1.17 +          (Literal(pol,pred)::lits, gen_union (op =) (ts, ts'))
    1.18        end;
    1.19  
    1.20  fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
    1.21 @@ -475,7 +475,7 @@
    1.22      val (cma, cnh) = count_constants clauses
    1.23      val params = (t_full, cma, cnh)
    1.24      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    1.25 -    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
    1.26 +    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (gen_union (op =)) [] tfree_litss)
    1.27      val _ =
    1.28        File.write_list file (
    1.29          map (#1 o (clause2tptp params)) axclauses @