src/HOL/Tools/ATP/res_clasimpset.ML
changeset 17764 fde495b9e24b
parent 17596 cd555d5a3254
child 17828 c82fb51ee18d
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Oct 05 10:56:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Oct 05 11:18:06 2005 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4      let val consts = consts_in_goal goal
     1.5  	fun relevant_axioms_aux1 cs k =
     1.6  	    let val thms1 = axioms_having_consts cs thmTab
     1.7 -		val cs1 = ResLib.flat_noDup (map consts_of_thm thms1)
     1.8 +		val cs1 = foldl (op union_string) [] (map consts_of_thm thms1)
     1.9  	    in
    1.10  		if ((cs1 subset cs) orelse n <= k) then (k,thms1) 
    1.11  		else (relevant_axioms_aux1 (cs1 union cs) (k+1))