# HG changeset patch
# User wenzelm
# Date 1427794764 -7200
# Node ID 9779b0c59ad4138cae21cb574b73cecec0a4d7e3
# Parent  3ecb48ce92d74138f80eec0f906c02e0c894a696
tuned;

diff -r 3ecb48ce92d7 -r 9779b0c59ad4 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Mar 31 11:16:55 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Mar 31 11:39:24 2015 +0200
@@ -737,7 +737,7 @@
 
 (*** Isabelle helpers ***)
 
-val local_prefix = "local" ^ Long_Name.separator
+val local_prefix = Long_Name.localN ^ Long_Name.separator
 
 fun elided_backquote_thm threshold th =
   elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)