1.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  *}
     1.5  
     1.6  theory Type_Encodings
     1.7 -imports Main
     1.8 +imports "~~/src/HOL/Sledgehammer2d"(*###*)
     1.9  begin
    1.10  
    1.11  declare [[metis_new_skolemizer]]

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.3 @@ -1444,9 +1444,8 @@
     2.4  fun type_tag_idempotence_fact type_enc =
     2.5    let
     2.6      fun var s = ATerm (`I s, [])
     2.7 -    (* Reconstruction in Metis is strangely dependent on these names. *)
     2.8 -    fun tag tm = ATerm (type_tag, [var "T", tm])
     2.9 -    val tagged_var = tag (var "A")
    2.10 +    fun tag tm = ATerm (type_tag, [var "A", tm])
    2.11 +    val tagged_var = tag (var "X")
    2.12    in
    2.13      Formula (type_tag_idempotence_helper_name, Axiom,
    2.14               eq_formula type_enc [] false (tag tagged_var) tagged_var,

     3.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
     3.3 @@ -78,7 +78,10 @@
     3.4    let val thy = Proof_Context.theory_of ctxt in
     3.5      case hol_clause_from_metis ctxt sym_tab old_skolems mth of
     3.6        Const (@{const_name HOL.eq}, _) $ _ $ t =>
     3.7 -      t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
     3.8 +      let
     3.9 +        val ct = cterm_of thy t
    3.10 +        val cT = ctyp_of_term ct
    3.11 +      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
    3.12      | Const (@{const_name disj}, _) $ t1 $ t2 =>
    3.13        (if can HOLogic.dest_not t1 then t2 else t1)
    3.14        |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial