cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -12,7 +12,6 @@
   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
   type 'a proof = 'a ATP_Proof.proof
   type locality = ATP_Translate.locality
-  type type_sys = ATP_Translate.type_sys
 
   datatype reconstructor =
     Metis |
@@ -29,18 +28,18 @@
   type one_line_params =
     play * string * (string * locality) list * minimize_command * int * int
   type isar_params =
-    bool * bool * int * type_sys * string Symtab.table * int list list * int
+    bool * bool * int * string Symtab.table * int list list * int
     * (string * locality) list vector * int Symtab.table * string proof * thm
   val repair_conjecture_shape_and_fact_names :
-    type_sys -> string -> int list list -> int
-    -> (string * locality) list vector -> int list
+    string -> int list list -> int -> (string * locality) list vector
+    -> int list
     -> int list list * int * (string * locality) list vector * int list
   val used_facts_in_atp_proof :
-    Proof.context -> type_sys -> int -> (string * locality) list vector
-    -> string proof -> (string * locality) list
+    Proof.context -> int -> (string * locality) list vector -> string proof
+    -> (string * locality) list
   val used_facts_in_unsound_atp_proof :
-    Proof.context -> type_sys -> int list list -> int
-    -> (string * locality) list vector -> 'a proof -> string list option
+    Proof.context -> int list list -> int -> (string * locality) list vector
+    -> 'a proof -> string list option
   val uses_typed_helpers : int list -> 'a proof -> bool
   val one_line_proof_text : one_line_params -> string
   val make_tvar : string -> typ
@@ -80,7 +79,7 @@
 type one_line_params =
   play * string * (string * locality) list * minimize_command * int * int
 type isar_params =
-  bool * bool * int * type_sys * string Symtab.table * int list list * int
+  bool * bool * int * string Symtab.table * int list list * int
   * (string * locality) list vector * int Symtab.table * string proof * thm
 
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
@@ -122,11 +121,9 @@
   #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
   #> fst
 
-fun maybe_unprefix_fact_number type_sys =
-  polymorphism_of_type_sys type_sys <> Polymorphic
-  ? (space_implode "_" o tl o space_explode "_")
+val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
 
-fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
+fun repair_conjecture_shape_and_fact_names output conjecture_shape
         fact_offset fact_names typed_helpers =
   if String.isSubstring set_ClauseFormulaRelationN output then
     let
@@ -139,7 +136,7 @@
         |> map (fn s => find_index (curry (op =) s) seq + 1)
       fun names_for_number j =
         j |> AList.lookup (op =) name_map |> these
-          |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys
+          |> map_filter (try (unascii_of o unprefix_fact_number
                               o unprefix fact_prefix))
           |> map (fn name =>
                      (name, name |> find_first_in_list_vector fact_names |> the)
@@ -158,16 +155,16 @@
 val extract_step_number =
   Int.fromString o perhaps (try (unprefix vampire_step_prefix))
 
-fun resolve_fact type_sys _ fact_names (_, SOME s) =
+fun resolve_fact _ fact_names (_, SOME s) =
     (case try (unprefix fact_prefix) s of
        SOME s' =>
-       let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in
+       let val s' = s' |> unprefix_fact_number |> unascii_of in
          case find_first_in_list_vector fact_names s' of
            SOME x => [(s', x)]
          | NONE => []
        end
      | NONE => [])
-  | resolve_fact _ facts_offset fact_names (num, NONE) =
+  | resolve_fact facts_offset fact_names (num, NONE) =
     (case extract_step_number num of
        SOME j =>
        let val j = j - facts_offset in
@@ -178,8 +175,7 @@
        end
      | NONE => [])
 
-fun is_fact type_sys conjecture_shape =
-  not o null o resolve_fact type_sys 0 conjecture_shape
+fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
 
 fun resolve_conjecture _ (_, SOME s) =
     (case try (unprefix conjecture_prefix) s of
@@ -215,29 +211,29 @@
   else
     isa_ext
 
-fun add_fact _ type_sys facts_offset fact_names (Inference (name, _, [])) =
-    union (op =) (resolve_fact type_sys facts_offset fact_names name)
-  | add_fact ctxt _ _ _ (Inference (_, _, deps)) =
+fun add_fact _ facts_offset fact_names (Inference (name, _, [])) =
+    union (op =) (resolve_fact facts_offset fact_names name)
+  | add_fact ctxt _ _ (Inference (_, _, deps)) =
     if AList.defined (op =) deps leo2_ext then
       insert (op =) (ext_name ctxt, General (* or Chained... *))
     else
       I
-  | add_fact _ _ _ _ _ = I
+  | add_fact _ _ _ _ = I
 
-fun used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof =
+fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof =
   if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names
-  else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
+  else fold (add_fact ctxt facts_offset fact_names) atp_proof []
 
 fun is_conjecture_used_in_proof conjecture_shape =
   exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
            | _ => false)
 
-fun used_facts_in_unsound_atp_proof _ _ _ _ _ [] = NONE
-  | used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
+fun used_facts_in_unsound_atp_proof _ _ _ _ [] = NONE
+  | used_facts_in_unsound_atp_proof ctxt conjecture_shape facts_offset
                                     fact_names atp_proof =
     let
       val used_facts =
-        used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
+        used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
     in
       if forall (is_locality_global o snd) used_facts andalso
          not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
@@ -653,12 +649,11 @@
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
-fun add_line _ _ _ (line as Definition _) lines = line :: lines
-  | add_line type_sys conjecture_shape fact_names (Inference (name, t, []))
-             lines =
+fun add_line _ _ (line as Definition _) lines = line :: lines
+  | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
-    if is_fact type_sys fact_names name then
+    if is_fact fact_names name then
       (* Facts are not proof lines. *)
       if is_only_type_information t then
         map (replace_dependencies_in_line (name, [])) lines
@@ -672,7 +667,7 @@
       Inference (name, s_not t, []) :: lines
     else
       map (replace_dependencies_in_line (name, [])) lines
-  | add_line _ _ _ (Inference (name, t, deps)) lines =
+  | add_line _ _ (Inference (name, t, deps)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
       Inference (name, t, deps) :: lines
@@ -700,13 +695,12 @@
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
-fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
+fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
-  | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names
-                     frees (Inference (name, t, deps)) (j, lines) =
+  | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
+                     (Inference (name, t, deps)) (j, lines) =
     (j + 1,
-     if is_fact type_sys fact_names name orelse
-        is_conjecture conjecture_shape name orelse
+     if is_fact fact_names name orelse is_conjecture conjecture_shape name orelse
         (* the last line must be kept *)
         j = 0 orelse
         (not (is_only_type_information t) andalso
@@ -741,24 +735,22 @@
 fun smart_case_split [] facts = ByMetis facts
   | smart_case_split proofs facts = CaseSplit (proofs, facts)
 
-fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names
-                             name =
-  if is_fact type_sys fact_names name then
-    apsnd (union (op =)
-          (map fst (resolve_fact type_sys facts_offset fact_names name)))
+fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
+  if is_fact fact_names name then
+    apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
   else
     apfst (insert (op =) (raw_label_for_name conjecture_shape name))
 
-fun step_for_line _ _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
-  | step_for_line _ conjecture_shape _ _ _ (Inference (name, t, [])) =
+fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
+  | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) =
     Assume (raw_label_for_name conjecture_shape name, t)
-  | step_for_line type_sys conjecture_shape facts_offset
-                  fact_names j (Inference (name, t, deps)) =
+  | step_for_line conjecture_shape facts_offset fact_names j
+                  (Inference (name, t, deps)) =
     Have (if j = 1 then [Show] else [],
           raw_label_for_name conjecture_shape name,
           fold_rev forall_of (map Var (Term.add_vars t [])) t,
-          ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape
-                                                  facts_offset fact_names)
+          ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
+                                                  fact_names)
                         deps ([], [])))
 
 fun repair_name "$true" = "c_True"
@@ -772,9 +764,8 @@
     else
       s
 
-fun isar_proof_from_atp_proof pool ctxt type_sys isar_shrink_factor
-        conjecture_shape facts_offset fact_names sym_tab params frees
-        atp_proof =
+fun isar_proof_from_atp_proof pool ctxt isar_shrink_factor conjecture_shape
+        facts_offset fact_names sym_tab params frees atp_proof =
   let
     val lines =
       atp_proof
@@ -782,15 +773,15 @@
       |> nasty_atp_proof pool
       |> map_term_names_in_atp_proof repair_name
       |> decode_lines ctxt sym_tab
-      |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names)
+      |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
       |> rpair (0, [])
-      |-> fold_rev (add_desired_line type_sys isar_shrink_factor
-                                     conjecture_shape fact_names frees)
+      |-> fold_rev (add_desired_line isar_shrink_factor conjecture_shape
+                                     fact_names frees)
       |> snd
   in
     (if null params then [] else [Fix params]) @
-    map2 (step_for_line type_sys conjecture_shape facts_offset fact_names)
+    map2 (step_for_line conjecture_shape facts_offset fact_names)
          (length lines downto 1) lines
   end
 
@@ -1084,8 +1075,8 @@
   in do_proof end
 
 fun isar_proof_text ctxt isar_proof_requested
-        (debug, full_types, isar_shrink_factor, type_sys, pool,
-         conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof, goal)
+        (debug, full_types, isar_shrink_factor, pool, conjecture_shape,
+         facts_offset, fact_names, sym_tab, atp_proof, goal)
         (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val isar_shrink_factor =
@@ -1095,7 +1086,7 @@
     val one_line_proof = one_line_proof_text one_line_params
     fun isar_proof_for () =
       case atp_proof
-           |> isar_proof_from_atp_proof pool ctxt type_sys isar_shrink_factor
+           |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor
                   conjecture_shape facts_offset fact_names sym_tab params frees
            |> redirect_proof hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof

--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -130,7 +130,8 @@
   val type_constrs_of_terms : theory -> term list -> string list
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_sys
-    -> bool -> bool -> term list -> term -> ((string * locality) * term) list
+    -> bool -> bool -> bool -> term list -> term
+    -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
        * (string * locality) list vector * int list * int Symtab.table
   val atp_problem_weights : string problem -> (string * real) list
@@ -1547,12 +1548,8 @@
    the remote provers might care. *)
 fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
                           (j, formula as {name, locality, kind, ...}) =
-  Formula (prefix ^
-           (if freshen andalso
-               polymorphism_of_type_sys type_sys <> Polymorphic then
-              string_of_int j ^ "_"
-            else
-              "") ^ encode name,
+  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
+           encode name,
            kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
            case locality of
              Intro => intro_info
@@ -1838,7 +1835,7 @@
 val explicit_apply = NONE (* for experimental purposes *)
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
-                        readable_names preproc hyp_ts concl_t facts =
+        freshen_facts readable_names preproc hyp_ts concl_t facts =
   let
     val (format, type_sys) = choose_format [format] type_sys
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
@@ -1877,8 +1874,8 @@
     val problem =
       [(explicit_declsN, sym_decl_lines),
        (factsN,
-        map (formula_line_for_fact ctxt format fact_prefix ascii_of true
-                                   nonmono_Ts type_sys)
+        map (formula_line_for_fact ctxt format fact_prefix ascii_of
+                                   freshen_facts nonmono_Ts type_sys)
             (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map formula_line_for_arity_clause arity_clauses),

--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -198,8 +198,8 @@
       tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false []
-                          @{prop False} props
+      prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false false
+                          [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jun 09 00:16:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jun 09 00:16:28 2011 +0200
@@ -649,8 +649,8 @@
                 val (atp_problem, pool, conjecture_offset, facts_offset,
                      fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                      type_sys (Config.get ctxt atp_readable_names) true hyp_ts
-                      concl_t facts
+                      type_sys true (Config.get ctxt atp_readable_names) true
+                      hyp_ts concl_t facts
                 fun weights () = atp_problem_weights atp_problem
                 val core =
                   File.shell_path command ^ " " ^
@@ -685,7 +685,7 @@
                 val (conjecture_shape, facts_offset, fact_names,
                      typed_helpers) =
                   if is_none outcome then
-                    repair_conjecture_shape_and_fact_names type_sys output
+                    repair_conjecture_shape_and_fact_names output
                         conjecture_shape facts_offset fact_names typed_helpers
                   else
                     (* don't bother repairing *)
@@ -693,7 +693,7 @@
                 val outcome =
                   case outcome of
                     NONE =>
-                    used_facts_in_unsound_atp_proof ctxt type_sys
+                    used_facts_in_unsound_atp_proof ctxt
                         conjecture_shape facts_offset fact_names atp_proof
                     |> Option.map (fn facts =>
                            UnsoundProof (is_type_sys_virtually_sound type_sys,
@@ -704,11 +704,11 @@
               in
                 ((pool, conjecture_shape, facts_offset, fact_names,
                   typed_helpers, sym_tab),
-                 (output, msecs, type_sys, atp_proof, outcome))
+                 (output, msecs, atp_proof, outcome))
               end
             val timer = Timer.startRealTimer ()
             fun maybe_run_slice blacklist slice
-                                (result as (_, (_, msecs0, _, _, SOME _))) =
+                                (result as (_, (_, msecs0, _, SOME _))) =
                 let
                   val time_left = Time.- (timeout, Timer.checkRealTimer timer)
                 in
@@ -716,18 +716,17 @@
                     result
                   else
                     (run_slice blacklist slice time_left
-                     |> (fn (stuff, (output, msecs, type_sys, atp_proof,
-                                     outcome)) =>
-                            (stuff, (output, int_opt_add msecs0 msecs, type_sys,
+                     |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
+                            (stuff, (output, int_opt_add msecs0 msecs,
                                      atp_proof, outcome))))
                 end
               | maybe_run_slice _ _ result = result
             fun maybe_blacklist_facts_and_retry iter blacklist
                     (result as ((_, _, facts_offset, fact_names, _, _),
-                                (_, _, type_sys, atp_proof,
+                                (_, _, atp_proof,
                                  SOME (UnsoundProof (false, _))))) =
-                (case used_facts_in_atp_proof ctxt type_sys facts_offset
-                                              fact_names atp_proof of
+                (case used_facts_in_atp_proof ctxt facts_offset fact_names
+                                              atp_proof of
                    [] => result
                  | new_baddies =>
                    if slicing andalso iter < atp_blacklist_max_iters - 1 then
@@ -741,8 +740,7 @@
               | maybe_blacklist_facts_and_retry _ _ result = result
           in
             ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
-             ("", SOME 0, hd fallback_best_type_systems, [],
-              SOME InternalError))
+             ("", SOME 0, [], SOME InternalError))
             |> fold (maybe_run_slice []) actual_slices
                (* The ATP found an unsound proof? Automatically try again
                   without the offending facts! *)
@@ -755,14 +753,14 @@
        the proof file too. *)
     fun cleanup prob_file =
       if dest_dir = "" then try File.rm prob_file else NONE
-    fun export prob_file (_, (output, _, _, _, _)) =
+    fun export prob_file (_, (output, _, _, _)) =
       if dest_dir = "" then
         ()
       else
         File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
     val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
           sym_tab),
-         (output, msecs, type_sys, atp_proof, outcome)) =
+         (output, msecs, atp_proof, outcome)) =
       with_path cleanup export run_on problem_path_name
     val important_message =
       if mode = Normal andalso
@@ -775,8 +773,7 @@
         NONE =>
         let
           val used_facts =
-            used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
-                                    atp_proof
+            used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof
         in
           (used_facts,
            fn () =>
@@ -792,9 +789,9 @@
               let
                 val full_types = uses_typed_helpers typed_helpers atp_proof
                 val isar_params =
-                  (debug, full_types, isar_shrink_factor, type_sys, pool,
-                   conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
-                   goal)
+                  (debug, full_types, isar_shrink_factor, pool,
+                   conjecture_shape, facts_offset, fact_names, sym_tab,
+                   atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command minimize_command name preplay,