src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML

   type minimize_command = string list -> string
   type metis_params =
     string * minimize_command * type_system * string proof * int
     * (string * locality) list vector * thm * int
   type isar_params =
-     Proof.context * bool * int * string Symtab.table * int list list
+    Proof.context * bool * int * string Symtab.table * int list list
+    * int Symtab.table
   type text_result = string * (string * locality) list
 
   val repair_conjecture_shape_and_fact_names :
     type_system -> string -> int list list -> int
     -> (string * locality) list vector

 type metis_params =
   string * minimize_command * type_system * string proof * int
   * (string * locality) list vector * thm * int
 type isar_params =
   Proof.context * bool * int * string Symtab.table * int list list
+  * int Symtab.table
 type text_result = string * (string * locality) list
 
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
 

     | _ => s
   end
 
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
-fun raw_term_from_pred thy type_sys tfrees =
+fun raw_term_from_pred thy sym_tab tfrees =
   let
     fun aux opt_T extra_us u =
       case u of
         ATerm (a, us) =>
         if String.isPrefix tff_type_prefix a then

               (* Vampire is keen on producing these. *)
               @{const True}
             else
               list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
           end
-        | SOME b =>
-          let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
-            if b = type_tag_name then
+        | SOME s =>
+          let val (s', mangled_us) = s |> unmangled_const |>> invert_const in
+            if s' = type_tag_name then
               case mangled_us @ us of
                 [typ_u, term_u] =>
                 aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
               | _ => raise FO_TERM us
-            else if b = predicator_base then
+            else if s' = predicator_base then
               aux (SOME @{typ bool}) [] (hd us)
-            else if b = explicit_app_base then
+            else if s' = explicit_app_base then
               aux opt_T (nth us 1 :: extra_us) (hd us)
-            else if b = type_pred_base then
+            else if s' = type_pred_base then
               @{const True} (* ignore type predicates *)
             else
               let
-                val num_ty_args = num_atp_type_args thy type_sys b
+                val num_ty_args =
+                  length us - the_default 0 (Symtab.lookup sym_tab s)
                 val (type_us, term_us) =
                   chop num_ty_args us |>> append mangled_us
                 (* Extra args from "hAPP" come after any arguments given
                    directly to the constant. *)
                 val term_ts = map (aux NONE []) term_us
                 val extra_ts = map (aux NONE []) extra_us
                 val T =
                   case opt_T of
                     SOME T => map fastype_of term_ts ---> T
                   | NONE =>
-                    if num_type_args thy b = length type_us then
+                    if num_type_args thy s' = length type_us then
                       Sign.const_instance thy
-                          (b, map (typ_from_fo_term tfrees) type_us)
+                          (s', map (typ_from_fo_term tfrees) type_us)
                     else
                       HOLogic.typeT
-                val b = unproxify_const b
-              in list_comb (Const (b, T), term_ts @ extra_ts) end
+                val s' = s' |> unproxify_const
+              in list_comb (Const (s', T), term_ts @ extra_ts) end
           end
         | NONE => (* a free or schematic variable *)
           let
             val ts = map (aux NONE []) (us @ extra_us)
             val T = map fastype_of ts ---> HOLogic.typeT

                     (* Skolem constants? *)
                     Var ((repair_atp_variable_name Char.toUpper a, 0), T)
           in list_comb (t, ts) end
   in aux (SOME HOLogic.boolT) [] end
 
-fun term_from_pred thy type_sys tfrees pos (u as ATerm (s, _)) =
+fun term_from_pred thy sym_tab tfrees pos (u as ATerm (s, _)) =
   if String.isPrefix class_prefix s then
     add_type_constraint pos (type_constraint_from_term tfrees u)
     #> pair @{const True}
   else
-    pair (raw_term_from_pred thy type_sys tfrees u)
+    pair (raw_term_from_pred thy sym_tab tfrees u)
 
 val combinator_table =
   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
    (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
    (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),

                   |> map Var
   in fold_rev quant_of vars t end
 
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    appear in the formula. *)
-fun prop_from_formula thy type_sys tfrees phi =
+fun prop_from_formula thy sym_tab tfrees phi =
   let
     fun do_formula pos phi =
       case phi of
         AQuant (_, [], phi) => do_formula pos phi
       | AQuant (q, (s, _) :: xs, phi') =>

              | AImplies => s_imp
              | AIf => s_imp o swap
              | AIff => s_iff
              | ANotIff => s_not o s_iff
              | _ => raise Fail "unexpected connective")
-      | AAtom tm => term_from_pred thy type_sys tfrees pos tm
+      | AAtom tm => term_from_pred thy sym_tab tfrees pos tm
       | _ => raise FORMULA [phi]
   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
 
 fun check_formula ctxt =
   Type.constraint HOLogic.boolT

 (**** Translation of TSTP files to Isar Proofs ****)
 
 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
 
-fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt =
+fun decode_line sym_tab tfrees (Definition (name, phi1, phi2)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
-      val t1 = prop_from_formula thy type_sys tfrees phi1
+      val t1 = prop_from_formula thy sym_tab tfrees phi1
       val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = prop_from_formula thy type_sys tfrees phi2
+      val t2 = prop_from_formula thy sym_tab tfrees phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> uncombine_term |> check_formula ctxt
         |> HOLogic.dest_eq
     in
       (Definition (name, t1, t2),
        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
-  | decode_line type_sys tfrees (Inference (name, u, deps)) ctxt =
+  | decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
-      val t = u |> prop_from_formula thy type_sys tfrees
+      val t = u |> prop_from_formula thy sym_tab tfrees
                 |> uncombine_term |> check_formula ctxt
     in
       (Inference (name, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     end
-fun decode_lines ctxt type_sys tfrees lines =
-  fst (fold_map (decode_line type_sys tfrees) lines ctxt)
+fun decode_lines ctxt sym_tab tfrees lines =
+  fst (fold_map (decode_line sym_tab tfrees) lines ctxt)
 
 fun is_same_inference _ (Definition _) = false
   | is_same_inference t (Inference (_, t', _)) = t aconv t'
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or

       "c_equal" (* seen in Vampire proofs *)
     else
       s
 
 fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
-        atp_proof conjecture_shape facts_offset fact_names params frees =
+        atp_proof conjecture_shape facts_offset fact_names sym_tab params
+        frees =
   let
     val lines =
       atp_proof
       |> nasty_atp_proof pool
       |> map_term_names_in_atp_proof repair_name
-      |> decode_lines ctxt type_sys tfrees
+      |> decode_lines ctxt sym_tab tfrees
       |> rpair [] |-> fold_rev (add_line type_sys 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)

         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
         do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
         (if n <> 1 then "next" else "qed")
   in do_proof end
 
-fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape)
+fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape,
+                     sym_tab)
                     (metis_params as (_, _, type_sys, atp_proof, facts_offset,
                                       fact_names, goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []

     val n = Logic.count_prems (prop_of goal)
     val (one_line_proof, lemma_names) = metis_proof_text metis_params
     fun isar_proof_for () =
       case isar_proof_from_atp_proof pool ctxt type_sys tfrees
                isar_shrink_factor atp_proof conjecture_shape facts_offset
-               fact_names params frees
+               fact_names sym_tab params frees
            |> redirect_proof hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof