--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 03 00:10:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 03 01:04:03 2011 +0200
@@ -754,8 +754,11 @@
the remote provers might care. *)
fun formula_line_for_fact ctxt prefix type_sys
(j, formula as {name, locality, kind, ...}) =
- Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
- formula_for_fact ctxt type_sys formula, NONE,
+ Formula (prefix ^
+ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
+ else string_of_int j ^ "_") ^
+ ascii_of name,
+ kind, formula_for_fact ctxt type_sys formula, NONE,
if generate_useful_info then
case locality of
Intro => useful_isabelle_info "intro"