tuned;
authorwenzelm
Tue, 31 Mar 2015 11:39:24 +0200
changeset 59875 9779b0c59ad4
parent 59874 3ecb48ce92d7
child 59876 8564d7abe5c5
tuned;
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)