author | blanchet |
Tue, 19 Feb 2013 13:27:33 +0100 | |
changeset 51183 | e0493414ce03 |
parent 51182 | 962190eab40d |
child 51184 | e2569dde59c8 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 19 13:21:49 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Feb 19 13:27:33 2013 +0100 @@ -1055,7 +1055,7 @@ else let val new_facts = - facts |> attach_parents_to_facts + facts |> attach_parents_to_facts [] |> filter_out (is_in_access_G o snd) val (learns, (n, _, _)) = ([], (0, next_commit_time (), false))