# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID faece9668bce4381d4848239779f4ed64efb3db1
# Parent  649bada59658b3f31f80d3a14ab90c271d102194
don't throw exception on unknown constants (e.g. skolems), and give more precise type to applied functions

diff -r 649bada59658 -r faece9668bce src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -476,13 +476,17 @@
                   chop num_ty_args us |>> append mangled_us
                 val term_ts = map (do_term [] NONE) term_us
                 val T =
-                  if not (null type_us) andalso
-                     num_type_args thy s' = length type_us then
-                    (s', map (typ_from_atp ctxt) type_us)
-                    |> Sign.const_instance thy
-                  else case opt_T of
-                    SOME T => map slack_fastype_of term_ts ---> T
-                  | NONE => HOLogic.typeT
+                  (if not (null type_us) andalso
+                      num_type_args thy s' = length type_us then
+                     try (Sign.const_instance thy)
+                         (s', map (typ_from_atp ctxt) type_us)
+                   else
+                     NONE)
+                  |> (fn SOME T => T
+                       | NONE => map slack_fastype_of term_ts --->
+                                 (case opt_T of
+                                    SOME T => T
+                                  | NONE => HOLogic.typeT))
                 val s' = s' |> unproxify_const
               in list_comb (Const (s', T), term_ts @ extra_ts) end
           end