handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes

--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -548,7 +548,7 @@
 
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    appear in the formula. *)
-fun prop_from_atp ctxt textual sym_tab phi =
+fun raw_prop_from_atp ctxt textual sym_tab phi =
   let
     fun do_formula pos phi =
       case phi of
@@ -581,6 +581,12 @@
   #> Syntax.check_term
          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
 
+fun prop_from_atp ctxt textual sym_tab =
+  let val thy = Proof_Context.theory_of ctxt in
+    raw_prop_from_atp ctxt textual sym_tab
+    #> uncombine_term thy #> infer_formula_types ctxt
+  end
+
 (**** Translation of TSTP files to Isar proofs ****)
 
 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
@@ -589,11 +595,12 @@
 fun decode_line sym_tab (Definition (name, phi1, phi2)) ctxt =
     let
       val thy = Proof_Context.theory_of ctxt
-      val t1 = prop_from_atp ctxt true sym_tab phi1
+      (* FIXME: prop or term? *)
+      val t1 = raw_prop_from_atp ctxt true sym_tab phi1
       val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = prop_from_atp ctxt true sym_tab phi2
+      val t2 = raw_prop_from_atp ctxt true sym_tab phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
@@ -603,11 +610,7 @@
        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
   | decode_line sym_tab (Inference (name, u, deps)) ctxt =
-    let
-      val thy = Proof_Context.theory_of ctxt
-      val t = u |> prop_from_atp ctxt true sym_tab
-                |> uncombine_term thy |> infer_formula_types ctxt
-    in
+    let val t = u |> prop_from_atp ctxt true sym_tab in
       (Inference (name, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     end

--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -9,6 +9,8 @@
 signature ATP_TRANSLATE =
 sig
   type 'a fo_term = 'a ATP_Problem.fo_term
+  type connective = ATP_Problem.connective
+  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
   type format = ATP_Problem.format
   type formula_kind = ATP_Problem.formula_kind
   type 'a problem = 'a ATP_Problem.problem
@@ -115,6 +117,8 @@
   val is_type_sys_fairly_sound : type_sys -> bool
   val choose_format : format list -> type_sys -> format * type_sys
   val raw_type_literals_for_types : typ list -> type_literal list
+  val mk_aconns :
+    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   val unmangled_const_name : string -> string
   val unmangled_const : string -> string * string fo_term list
   val translate_atp_fact :

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -17,8 +17,8 @@
   val trace_msg : Proof.context -> (unit -> string) -> unit
   val verbose : bool Config.T
   val verbose_warning : Proof.context -> string -> unit
-  val hol_term_from_metis :
-    Proof.context -> mode -> int Symtab.table -> Metis_Term.term -> term
+  val hol_clause_from_metis_MX :
+    Proof.context -> int Symtab.table -> Metis_Literal.literal list -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   val untyped_aconv : term * term -> bool
   val replay_one_inference :
@@ -230,6 +230,15 @@
   | hol_term_from_metis ctxt FT _ = hol_term_from_metis_FT ctxt
   | hol_term_from_metis ctxt MX sym_tab = hol_term_from_metis_MX ctxt sym_tab
 
+fun atp_literal_from_metis (pos, atom) =
+  atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
+fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
+  | atp_clause_from_metis lits =
+    lits |> map atp_literal_from_metis |> mk_aconns AOr
+
+fun hol_clause_from_metis_MX ctxt sym_tab =
+  atp_clause_from_metis #> prop_from_atp ctxt false sym_tab
+
 fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
   let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms
       val _ = trace_msg ctxt (fn () => "  calling type inference:")

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -57,27 +57,21 @@
 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
   | used_axioms _ _ = NONE
 
-fun cterm_from_metis ctxt sym_tab wrap tm =
-  let val thy = Proof_Context.theory_of ctxt in
-    tm |> hol_term_from_metis ctxt MX sym_tab |> wrap
-       |> Syntax.check_term
-              (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
-       |> cterm_of thy
-  end
-
 (* Lightweight predicate type information comes in two flavors, "t = t'" and
    "t => t'", where "t" and "t'" are the same term modulo type tags.
    In Isabelle, type tags are stripped away, so we are left with "t = t" or
    "t => t". *)
 fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth =
-  (case Metis_LiteralSet.toList (Metis_Thm.clause mth) of
-     [(true, (_, [_, tm]))] =>
-     tm |> cterm_from_metis ctxt sym_tab I |> Thm.reflexive
-     RS @{thm meta_eq_to_obj_eq}
-   | [_, (_, tm)] =>
-     tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab HOLogic.mk_Trueprop
-        |> Thm.trivial
-   | _ => raise Fail "unexpected tags sym clause")
+  let val thy = Proof_Context.theory_of ctxt in
+    case hol_clause_from_metis_MX ctxt sym_tab
+             (Metis_LiteralSet.toList (Metis_Thm.clause mth)) of
+      Const (@{const_name HOL.eq}, _) $ _ $ t =>
+      t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
+    | Const (@{const_name disj}, _) $ t1 $ t2 =>
+      (if can HOLogic.dest_not t1 then t2 else t1)
+      |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
+    | _ => raise Fail "unexpected tags sym clause"
+  end
   |> Meson.make_meta_clause
 
 val clause_params =