Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
imported patch metis_reconstr_give_type_infer_a_chance
authorblanchet
Mon, 06 Jun 2011 20:36:35 +0200
changeset 43200 ca7b0a48515d
parent 43199 45f33d290615
child 43201 0c9bf1a8e0d8
imported patch metis_reconstr_give_type_infer_a_chance
src/HOL/Tools/ATP/atp_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle