compile
authorblanchet
Tue, 19 Feb 2013 13:27:33 +0100
changeset 51183 e0493414ce03
parent 51182 962190eab40d
child 51184 e2569dde59c8
compile
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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))