src/HOL/Tools/ATP/atp_reconstruct.ML

                   |> 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 raw_prop_from_atp ctxt textual sym_tab phi =
+fun prop_from_atp ctxt textual sym_tab phi =
   let
     fun do_formula pos phi =
       case phi of
         AQuant (_, [], phi) => do_formula pos phi
       | AQuant (q, (s, _) :: xs, phi') =>

 fun infer_formula_types ctxt =
   Type.constraint HOLogic.boolT
   #> Syntax.check_term
          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
 
-fun prop_from_atp ctxt textual sym_tab =
+fun uncombined_etc_prop_from_atp ctxt textual sym_tab =
   let val thy = Proof_Context.theory_of ctxt in
-    raw_prop_from_atp ctxt textual sym_tab
+    prop_from_atp ctxt textual sym_tab
     #> textual ? uncombine_term thy #> infer_formula_types ctxt
   end
 
 (**** Translation of TSTP files to Isar proofs ****)
 

   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
 
 fun decode_line sym_tab (Definition (name, phi1, phi2)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
-      (* FIXME: prop or term? *)
-      val t1 = raw_prop_from_atp ctxt true sym_tab phi1
+      val t1 = prop_from_atp ctxt true sym_tab phi1
       val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = raw_prop_from_atp ctxt true sym_tab phi2
+      val t2 = prop_from_atp ctxt true sym_tab phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
         |> HOLogic.dest_eq
     in
       (Definition (name, t1, t2),
        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
   | decode_line sym_tab (Inference (name, u, deps)) ctxt =
-    let val t = u |> prop_from_atp ctxt true sym_tab in
+    let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in
       (Inference (name, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     end
 fun decode_lines ctxt sym_tab lines =
   fst (fold_map (decode_line sym_tab) lines ctxt)