# HG changeset patch
# User blanchet
# Date 1316701847 -7200
# Node ID 89341b8974123749eebf32c6df6146ecc766d92c
# Parent  0523a6be8ade96e8ee302a5a497ec45cfdd320d0
better type reconstruction -- prevents ill-instantiations in proof replay

diff -r 0523a6be8ade -r 89341b897412 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Sep 22 10:02:16 2011 -0400
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Thu Sep 22 16:30:47 2011 +0200
@@ -430,8 +430,12 @@
           end
         | NONE => (* a free or schematic variable *)
           let
-            val ts = map (do_term [] NONE) us @ extra_ts
-            val T = map slack_fastype_of ts ---> HOLogic.typeT
+            val term_ts = map (do_term [] NONE) us
+            val ts = term_ts @ extra_ts
+            val T =
+              case opt_T of
+                SOME T => map slack_fastype_of term_ts ---> T
+              | NONE => map slack_fastype_of ts ---> HOLogic.typeT
             val t =
               case strip_prefix_and_unascii fixed_var_prefix s of
                 SOME s =>
diff -r 0523a6be8ade -r 89341b897412 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Sep 22 10:02:16 2011 -0400
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Sep 22 16:30:47 2011 +0200
@@ -119,8 +119,6 @@
       val dischargers = map (fst o snd) th_cls_pairs
       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
-      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
-      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
       val type_enc = type_enc_from_string Sound type_enc
       val (sym_tab, axioms, old_skolems) =
@@ -129,6 +127,8 @@
           reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
         | get_isa_thm _ (Isa_Raw ith) = ith
       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
+      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
+      val _ = app (fn (_, th) => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) axioms
       val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
       val thms = axioms |> map fst
       val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
diff -r 0523a6be8ade -r 89341b897412 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Sep 22 10:02:16 2011 -0400
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Sep 22 16:30:47 2011 +0200
@@ -202,7 +202,8 @@
                clauses ([], [])
     (*
     val _ =
-      tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props))
+      tracing ("PROPS:\n" ^
+               cat_lines (map (Syntax.string_of_term ctxt o snd) props))
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false no_lambdasN