--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 30 19:15:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Sep 30 20:44:53 2010 +0200
@@ -77,8 +77,8 @@
only: bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-val abs_name = "Sledgehammer.abs"
-val skolem_prefix = "Sledgehammer.sko"
+val abs_name = sledgehammer_prefix ^ "abs"
+val skolem_prefix = sledgehammer_prefix ^ "sko"
val theory_const_suffix = Long_Name.separator ^ " 1"
fun repair_name reserved multi j name =