# HG changeset patch
# User blanchet
# Date 1351778448 -3600
# Node ID dbbf9578e7127fdf8ca0b7e395dbe2ad27028c7e
# Parent  64c8d9d3af186f6af708129f1803550cd18f8770
made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)

diff -r 64c8d9d3af18 -r dbbf9578e712 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 01 13:32:57 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 01 15:00:48 2012 +0100
@@ -783,7 +783,8 @@
     else
       let
         val all_names =
-          facts |> map snd |> map (rpair () o nickname_of) |> Symtab.make
+          Symtab.empty
+          |> fold Symtab.update (facts |> map (rpair () o nickname_of o snd))
         fun deps_of status th =
           if status = Non_Rec_Def orelse status = Rec_Def then
             SOME []