equal
deleted
inserted
replaced
66 |
66 |
67 fun relevant_axioms goal thmTab n = |
67 fun relevant_axioms goal thmTab n = |
68 let val consts = consts_in_goal goal |
68 let val consts = consts_in_goal goal |
69 fun relevant_axioms_aux1 cs k = |
69 fun relevant_axioms_aux1 cs k = |
70 let val thms1 = axioms_having_consts cs thmTab |
70 let val thms1 = axioms_having_consts cs thmTab |
71 val cs1 = ResLib.flat_noDup (map consts_of_thm thms1) |
71 val cs1 = foldl (op union_string) [] (map consts_of_thm thms1) |
72 in |
72 in |
73 if ((cs1 subset cs) orelse n <= k) then (k,thms1) |
73 if ((cs1 subset cs) orelse n <= k) then (k,thms1) |
74 else (relevant_axioms_aux1 (cs1 union cs) (k+1)) |
74 else (relevant_axioms_aux1 (cs1 union cs) (k+1)) |
75 end |
75 end |
76 |
76 |