--- 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