# HG changeset patch
# User blanchet
# Date 1357332979 -3600
# Node ID b2e7490a1b3d4a4b909709e93302ab336476446b
# Parent  72624ff45676ea48730ba02f3675d5c678d0b9e0
tweaked nicknames

diff -r 72624ff45676 -r b2e7490a1b3d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 21:24:47 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 04 21:56:19 2013 +0100
@@ -413,9 +413,8 @@
       (* There must be a better way to detect local facts. *)
       case try (unprefix local_prefix) hint of
         SOME suf =>
-        Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^
-        Long_Name.separator ^ suf ^ Long_Name.separator ^
-        elided_backquote_thm 50 th
+        Context.theory_name (Thm.theory_of_thm th) ^ Long_Name.separator ^ suf ^
+        Long_Name.separator ^ elided_backquote_thm 50 th
       | NONE => hint
     end
   else