src/HOL/Tools/ATP/atp_proof_reconstruct.ML

           val tm = do_term NONE term
         in quantify_over_var true lambda' var_name typ tm end
       | ATerm ((s, tys), us) =>
         if s = ""
         then error "Isar proof reconstruction failed because the ATP proof \
-                     \contains unparsable material."
+                     \contains unparsable material"
         else if s = tptp_equal then
           list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}),
             map (do_term NONE) us)
         else if not (null us) then
           let

     fun do_term extra_ts opt_T u =
       (case u of
         ATerm ((s, tys), us) =>
         if s = "" then
           error "Isar proof reconstruction failed because the ATP proof contains unparsable \
-            \material."
+            \material"
         else if String.isPrefix native_type_prefix s then
           @{const True} (* ignore TPTP type information (needed?) *)
         else if s = tptp_equal then
           list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}),
             map (do_term [] NONE) us)

             in list_comb (t, ts) end))
   in do_term [] end
 
 fun term_of_atp ctxt (ATP_Problem.THF _) type_enc =
     if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt)
-    else error "Unsupported Isar reconstruction."
+    else error "Unsupported Isar reconstruction"
   | term_of_atp ctxt _ type_enc =
     if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt
-    else error "Unsupported Isar reconstruction."
+    else error "Unsupported Isar reconstruction"
 
 fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) =
   if String.isPrefix class_prefix s then
     add_type_constraint pos (type_constraint_of_term ctxt u)
     #> pair @{const True}