# HG changeset patch
# User blanchet
# Date 1361276853 -3600
# Node ID e0493414ce03102a2e7dcf318d1afd9595f61610
# Parent  962190eab40dfa116ca828e505a1ec85f82389ed
compile

diff -r 962190eab40d -r e0493414ce03 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))