# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID ca7b0a48515df527ac036f0f6dbebaf51a163c8b
# Parent  45f33d2906156459ee9535021bacb3e93a4a22c4
imported patch metis_reconstr_give_type_infer_a_chance

diff -r 45f33d290615 -r ca7b0a48515d 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
@@ -482,8 +482,10 @@
                      let val Ts = type_us |> map (typ_from_atp ctxt) in
                        if new_skolem then
                          SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
+                       else if textual then
+                         try (Sign.const_instance thy) (s', Ts)
                        else
-                         try (Sign.const_instance thy) (s', Ts)
+                         NONE
                      end
                    else
                      NONE)