Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)
authorblanchet
Thu, 01 Nov 2012 15:00:48 +0100
changeset 49997 dbbf9578e712
parent 49996 64c8d9d3af18
child 49998 ad8a6db0b480
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)
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML file | annotate | diff | comparison | revisions 
--- 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 []
isabelle