changeset 52034 | 11b48e7a4e7e |
parent 52031 | 9a9238342963 |
child 52077 | 788b27dfaefa |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu May 16 14:27:43 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu May 16 14:58:30 2013 +0200 @@ -284,7 +284,7 @@ apsnd (union (op =) (map fst (resolve_fact fact_names ss))) else apfst (insert (op =) (label_of_clause names)) - | add_fact_of_dependencies fact_names names = + | add_fact_of_dependencies _ names = apfst (insert (op =) (label_of_clause names)) fun repair_name "$true" = "c_True"