avoid generating several formulas with the same name ("tfrees")
authorblanchet
Sun Oct 10 18:42:13 2010 +0700 (2010-10-10)
changeset 399757c50d5ca5c04
parent 39974 b525988432e9
child 39976 2474347538b8
avoid generating several formulas with the same name ("tfrees")
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Oct 06 10:49:27 2010 -0700
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Sun Oct 10 18:42:13 2010 +0700
     1.3 @@ -13,10 +13,6 @@
     1.4  
     1.5    val axiom_prefix : string
     1.6    val conjecture_prefix : string
     1.7 -  val helper_prefix : string
     1.8 -  val class_rel_clause_prefix : string
     1.9 -  val arity_clause_prefix : string
    1.10 -  val tfrees_name : string
    1.11    val prepare_axiom :
    1.12      Proof.context -> (string * 'a) * thm
    1.13      -> term * ((string * 'a) * fol_formula) option
    1.14 @@ -38,7 +34,7 @@
    1.15  val helper_prefix = "help_"
    1.16  val class_rel_clause_prefix = "clrel_";
    1.17  val arity_clause_prefix = "arity_"
    1.18 -val tfrees_name = "tfrees"
    1.19 +val tfree_prefix = "tfree_"
    1.20  
    1.21  (* Freshness almost guaranteed! *)
    1.22  val sledgehammer_weak_prefix = "Sledgehammer:"
    1.23 @@ -363,13 +359,13 @@
    1.24  fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
    1.25    map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
    1.26  
    1.27 -fun problem_line_for_free_type lit =
    1.28 -  Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
    1.29 +fun problem_line_for_free_type j lit =
    1.30 +  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
    1.31  fun problem_lines_for_free_types conjectures =
    1.32    let
    1.33      val litss = map free_type_literals_for_conjecture conjectures
    1.34      val lits = fold (union (op =)) litss []
    1.35 -  in map problem_line_for_free_type lits end
    1.36 +  in map2 problem_line_for_free_type (0 upto length lits - 1) lits end
    1.37  
    1.38  (** "hBOOL" and "hAPP" **)
    1.39