# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID 30ea62ab4f166cc8f72fd35518baf04fe5ec5b22
# Parent  7b6629037127898303d4a00ac8a4c82e4ab76994
made reconstruction of type tag equalities "\?x = \?x" reliable

diff -r 7b6629037127 -r 30ea62ab4f16 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Aug 22 15:02:45 2011 +0200
@@ -9,7 +9,7 @@
 *}
 
 theory Type_Encodings
-imports Main
+imports "~~/src/HOL/Sledgehammer2d"(*###*)
 begin
 
 declare [[metis_new_skolemizer]]
diff -r 7b6629037127 -r 30ea62ab4f16 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -1444,9 +1444,8 @@
 fun type_tag_idempotence_fact type_enc =
   let
     fun var s = ATerm (`I s, [])
-    (* Reconstruction in Metis is strangely dependent on these names. *)
-    fun tag tm = ATerm (type_tag, [var "T", tm])
-    val tagged_var = tag (var "A")
+    fun tag tm = ATerm (type_tag, [var "A", tm])
+    val tagged_var = tag (var "X")
   in
     Formula (type_tag_idempotence_helper_name, Axiom,
              eq_formula type_enc [] false (tag tagged_var) tagged_var,
diff -r 7b6629037127 -r 30ea62ab4f16 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -78,7 +78,10 @@
   let val thy = Proof_Context.theory_of ctxt in
     case hol_clause_from_metis ctxt sym_tab old_skolems mth of
       Const (@{const_name HOL.eq}, _) $ _ $ t =>
-      t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
+      let
+        val ct = cterm_of thy t
+        val cT = ctyp_of_term ct
+      in refl |> Drule.instantiate' [SOME cT] [SOME ct] end
     | Const (@{const_name disj}, _) $ t1 $ t2 =>
       (if can HOLogic.dest_not t1 then t2 else t1)
       |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial